subset_mul_closure_one — Mathlib

English

For any MulOneClass G and any subset S, S is contained in S · closure({1}).

Русский

Для любой группы с единицей и любого подмножества S выполняется S ⊆ S · closure({1}).

LaTeX

$$$\\forall S \\subseteq G,\\ S \\subseteq S \\cdot \\overline{\\{1\\}}$$$

Lean4

@[to_additive]
theorem subset_mul_closure_one {G} [MulOneClass G] [TopologicalSpace G] (s : Set G) : s ⊆ s * (closure { 1 } : Set G) :=
  by
  have : s ⊆ s * ({ 1 } : Set G) := by simp
  exact this.trans (smul_subset_smul_left subset_closure)

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