English
x specializes to y (notation x ⤳ y) if any of several equivalent properties hold, in particular 𝓝 x ≤ 𝓝 y.
Русский
x специализируется на y (обозначение x ⤳ y) если выполняется одно из эквивалентных условий, в частности 𝓝 x ≤ 𝓝 y.
LaTeX
$$$\text{Specializes}(x,y) \iff 𝓝 x \le 𝓝 y$$$
Lean4
/-- `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`. -/
def Specializes (x y : X) : Prop :=
𝓝 x ≤ 𝓝 y
