singletons_open_iff_discrete — Mathlib

English

Deprecated: equivalence between every singleton being open and discrete topology.

Русский

Устаревшее: эквивалентность между открытостью каждого единичного множества и дискретной топологией.

LaTeX

$$[deprecated] $(\forall a, IsOpen({a})) \iff DiscreteTopology( X )$$$

Lean4

@[deprecated discreteTopology_iff_isOpen_singleton (since := "2025-10-10")]
theorem singletons_open_iff_discrete {X : Type*} [TopologicalSpace X] :
    (∀ a : X, IsOpen ({ a } : Set X)) ↔ DiscreteTopology X :=
  discreteTopology_iff_isOpen_singleton.symm

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