mul_closure_one_eq — Mathlib

English

If F is closed, then F · closure({1}) = F.

Русский

Если F замкнутое, то F · closure({1}) = F.

LaTeX

$$$\\forall F \\subseteq G,\\ (\\text{IsClosed}(F)) \\Rightarrow F \\cdot \\overline{\\{1\\}} = F$$$

Lean4

@[to_additive]
theorem mul_closure_one_eq {F : Set G} (hF : IsClosed F) : F * (closure { 1 } : Set G) = F :=
  by
  refine Subset.antisymm ?_ (subset_mul_closure_one F)
  calc
    F * (closure { 1 } : Set G) = closure F * closure ({ 1 } : Set G) := by rw [hF.closure_eq]
    _ ⊆ closure (F * ({ 1 } : Set G)) := (smul_set_closure_subset _ _)
    _ = F := by simp

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