of_finite_of_isClosed_singleton — Mathlib

English

If α is finite and every singleton {a} is closed, then α carries the discrete topology.

Русский

Если множество α конечно и каждое единичное множество {a} замкнуто, то топология на α дискретна.

LaTeX

$$$[Finite(α)]\to(\forall a:\alpha, IsClosed({a}) ) \Rightarrow DiscreteTopology(α)$$$

Lean4

theorem of_finite_of_isClosed_singleton [TopologicalSpace α] [Finite α] (h : ∀ a : α, IsClosed { a }) :
    DiscreteTopology α :=
  discreteTopology_iff_forall_isClosed.mpr fun s ↦ s.iUnion_of_singleton_coe ▸ isClosed_iUnion_of_finite fun _ ↦ h _

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