discreteTopology_of_isOpen_singleton_one

English

If the singleton {1} is open in G, then G has the discrete topology.

Русский

Если множество {1} открыто в G, то топология G дискретна.

LaTeX

$$$IsOpen\\left(\\{1\\}\\right) \\Rightarrow DiscreteTopology(G).$$$

Lean4

@[to_additive]
theorem discreteTopology_of_isOpen_singleton_one (h : IsOpen ({ 1 } : Set G)) : DiscreteTopology G :=
  by
  rw [discreteTopology_iff_isOpen_singleton]
  intro g
  suffices { g } = (g⁻¹ * ·) ⁻¹' { 1 } by
    rw [this]
    exact (continuous_mul_left g⁻¹).isOpen_preimage _ h
  simp only [mul_one, Set.preimage_mul_left_singleton, inv_inv]

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