specializationOrder — Mathlib

English

On a T0 space, the specialization relation defines a partial order on X.

Русский

На T0-пространстве отношение специализации образует частичный порядок на X.

LaTeX

$$$\text{specializationOrder}(X) \text{ is a PartialOrder on } X \text{ when } [TopologicalSpace X][T0Space X].$$$

Lean4

/-- Specialization forms a partial order on a t0 topological space. -/
def specializationOrder (X) [TopologicalSpace X] [T0Space X] : PartialOrder X :=
  { specializationPreorder X, PartialOrder.lift (OrderDual.toDual ∘ 𝓝) nhds_injective with }

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