discreteTopology_iff_forall_isOpen

English

A space is discrete if and only if every subset is open.

Русский

Пространство дискретно тогда и только тогда, когда каждая подмножество открыто.

LaTeX

$$$DiscreteTopology(\alpha) \iff \forall S \subseteq \alpha,\ IsOpen(S)$$$

Lean4

theorem discreteTopology_iff_forall_isOpen [TopologicalSpace α] : DiscreteTopology α ↔ ∀ s : Set α, IsOpen s :=
  ⟨@isOpen_discrete _ _, fun h ↦ ⟨eq_bot_of_singletons_open fun _ ↦ h _⟩⟩

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