Theorems · Definition · general topology

Specializes

{X : Type u_1} → [TopologicalSpace X] → X → X → Prop

x specializes to y (notation: x ⤳ y) if either of the following equivalent properties hold: * 𝓝 x ≤ 𝓝 y; this property is used as the definition; * pure x ≤ 𝓝 y; in other words, any neighbourhood of y contains x; * y ∈ closure {x}; * closure {y} ⊆ closure {x}; * for any closed set s we have x ∈ s → y ∈ s; * for any open set s we have y ∈ s → x ∈ s; * y is a cluster point of the filter pure x = 𝓟 {x}. This relation defines a Preorder on X. If X is a T₀ space, then this preorder is a partial order. If X is a T₁ space, then this partial order is trivial : x ⤳ y ↔ x = y.

Defined in

Mathlib.Topology.Defs.Filter

Cited by

176 results in Mathlib

Foundations

Depth 19 from the axioms, rests on 92 definitions · uses propext, Quot.sound

Assumes

TopologicalSpace