English
Two points x and y are inseparable if their neighborhood filters are equal, i.e. 𝓝 x = 𝓝 y.
Русский
Две точки x и y неразделимы, если их фильтры окрестностей совпадают: 𝓝 x = 𝓝 y.
LaTeX
$$$𝓝 x = 𝓝 y$$$
Lean4
/-- Two points `x` and `y` in a topological space are `Inseparable` if any of the following
equivalent properties hold:
- `𝓝 x = 𝓝 y`; we use this property as the definition;
- for any open set `s`, `x ∈ s ↔ y ∈ s`, see `inseparable_iff_forall_isOpen`;
- for any closed set `s`, `x ∈ s ↔ y ∈ s`, see `inseparable_iff_forall_isClosed`;
- `x ∈ closure {y}` and `y ∈ closure {x}`, see `inseparable_iff_mem_closure`;
- `closure {x} = closure {y}`, see `inseparable_iff_closure_eq`.
-/
def Inseparable (x y : X) : Prop :=
𝓝 x = 𝓝 y
