discreteTopology_iff_isOpen_singleton

English

A space is discrete if and only if every singleton {a} is open.

Русский

Пространство дискретно тогда и только тогда, когда каждое множество-единичный {a} открыто.

LaTeX

$$$DiscreteTopology(\alpha) \iff \forall a:\alpha, IsOpen({a})$$$

Lean4

theorem discreteTopology_iff_isOpen_singleton [TopologicalSpace α] :
    DiscreteTopology α ↔ (∀ a : α, IsOpen ({ a } : Set α)) :=
  ⟨fun _ _ ↦ isOpen_discrete _, fun h ↦ ⟨eq_bot_of_singletons_open h⟩⟩

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