locallyCompactSpace_of_mem_nhds_of_group

English

If K is compact, then K · closure({1}) = closure(K). (Repeated statement of 195207)

Русский

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

LaTeX

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

Lean4

/-- If a point in a topological group has a compact neighborhood, then the group is
locally compact. -/
@[to_additive]
theorem locallyCompactSpace_of_mem_nhds_of_group {K : Set G} (hK : IsCompact K) {x : G} (h : K ∈ 𝓝 x) :
    LocallyCompactSpace G := by
  suffices WeaklyLocallyCompactSpace G from inferInstance
  refine ⟨fun y ↦ ⟨(y * x⁻¹) • K, ?_, ?_⟩⟩
  · exact hK.smul _
  · rw [← preimage_smul_inv]
    exact (continuous_const_smul _).continuousAt.preimage_mem_nhds (by simpa using h)

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