Theorems · Theorem · general topology

specializes_TFAE

∀ {X : Type u_1} [inst : TopologicalSpace X] (x y : X),
  [x ⤳ y, pure x ≤ nhds y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s,
      y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)].TFAE

A collection of equivalent definitions of x ⤳ y. The public API is given by iff lemmas below.

Defined in

Mathlib.Topology.Inseparable

Cited by

6 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace