subset_mul_self — Mathlib

English

If U ∈ B then U ⊆ U · U; i.e., every element of U can be written as a product of two elements from U (with the identity in U).

Русский

Если U ∈ B, то U ⊆ U · U; то есть каждый элемент из U может быть записан как произведение двух элементов из U.

LaTeX

$$∀ {G} [Group G] (B : GroupFilterBasis G) {U : Set G}, U ∈ B → U ⊆ U * U$$

Lean4

@[to_additive]
theorem subset_mul_self (B : GroupFilterBasis G) {U : Set G} (h : U ∈ B) : U ⊆ U * U := fun x x_in ↦
  ⟨1, one h, x, x_in, one_mul x⟩

Похожие утверждения