English
If M is a GroupWithZero equipped with a topology that makes the multiplication continuous, and M is compact and T1, then the singleton {0} is open.
Русский
Если M является группой с нулём и имеет топологию, при которой умножение непрочно, и если M компактна и T1, то множество {0} открыто.
LaTeX
$$$IsOpen\left\{0\right\}$$$
Lean4
theorem isOpen_singleton_zero [GroupWithZero M] [TopologicalSpace M] [ContinuousMul M] [CompactSpace M] [T1Space M] :
IsOpen {(0 : M)} := by
obtain ⟨U, hU, h0U, h1U⟩ := t1Space_iff_exists_open.mp ‹_› zero_ne_one
obtain ⟨W, hW, hW'⟩ := exists_mem_nhds_zero_mul_subset isCompact_univ (hU.mem_nhds h0U)
by_cases H : ∃ x ≠ 0, x ∈ W
· obtain ⟨x, hx, hxW⟩ := H
cases h1U (hW' (by simpa [hx] using Set.mul_mem_mul (Set.mem_univ x⁻¹) hxW))
· obtain rfl : W = {0} := subset_antisymm (by simpa [not_imp_not] using H) (by simpa using mem_of_mem_nhds hW)
simpa [isOpen_iff_mem_nhds]
