discreteTopology_iff_forall_isClosed

English

Discrete topology is equivalent to every subset being closed.

Русский

Дискретная топология эквивалентна тому, что каждое подмножество замкнуто.

LaTeX

$$$DiscreteTopology(\alpha) \iff \forall S: Set(\alpha), IsClosed(S)$$$

Lean4

theorem discreteTopology_iff_forall_isClosed [TopologicalSpace α] : DiscreteTopology α ↔ ∀ s : Set α, IsClosed s :=
  discreteTopology_iff_forall_isOpen.trans <| compl_surjective.forall.trans <| forall_congr' fun _ ↦ isOpen_compl_iff

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