mul_closure_one_eq_closure — Mathlib

English

If K is compact, then K · closure({1}) = closure(K).

Русский

Если K компактно, то K · closure({1}) = closure(K).

LaTeX

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

Lean4

@[to_additive]
theorem mul_closure_one_eq_closure {K : Set G} (hK : IsCompact K) : K * (closure { 1 } : Set G) = closure K :=
  by
  apply Subset.antisymm ?_ ?_
  ·
    calc
      K * (closure { 1 } : Set G) ⊆ closure K * (closure { 1 } : Set G) := smul_subset_smul_right subset_closure
      _ ⊆ closure (K * ({ 1 } : Set G)) := (smul_set_closure_subset _ _)
      _ = closure K := by simp
  · have : IsClosed (K * (closure { 1 } : Set G)) := IsClosed.smul_left_of_isCompact isClosed_closure hK
    rw [IsClosed.closure_subset_iff this]
    exact subset_mul_closure_one K

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