English
Every separable weakly locally compact topological group is σ-compact.
Русский
Каждая сепарабельная слабопроизвольная локально компактная топологическая группа является σ-компактной.
LaTeX
$$$G \text{ is } \Sigma\text{-compact.}$$$
Lean4
/-- Every weakly locally compact separable topological group is σ-compact.
Note: this is not true if we drop the topological group hypothesis. -/
@[to_additive SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace /--
Every weakly locally compact separable topological additive group is σ-compact.
Note: this is not true if we drop the topological group hypothesis. -/
]
instance (priority := 100) sigmaCompactSpace [SeparableSpace G] [WeaklyLocallyCompactSpace G] : SigmaCompactSpace G :=
by
obtain ⟨L, hLc, hL1⟩ := exists_compact_mem_nhds (1 : G)
refine ⟨⟨fun n => (fun x => x * denseSeq G n) ⁻¹' L, ?_, ?_⟩⟩
· intro n
exact (Homeomorph.mulRight _).isCompact_preimage.mpr hLc
· refine iUnion_eq_univ_iff.2 fun x => ?_
obtain ⟨_, ⟨n, rfl⟩, hn⟩ : (range (denseSeq G) ∩ (fun y => x * y) ⁻¹' L).Nonempty :=
by
rw [← (Homeomorph.mulLeft x).apply_symm_apply 1] at hL1
exact (denseRange_denseSeq G).inter_nhds_nonempty ((Homeomorph.mulLeft x).continuous.continuousAt <| hL1)
exact ⟨n, hn⟩
