Theorems · Definition · general topology

Inseparable

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

Two points x and y in a topological space are Inseparable, or topologically indistinguishable, 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.

Defined in

Mathlib.Topology.Defs.Filter

Cited by

160 results in Mathlib

Foundations

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

Assumes

TopologicalSpace