mathlib3 documentation

topology.inseparable

Inseparable points in a topological space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define

We also prove various basic properties of the relation inseparable.

Notations #

Tags #

topological space, separation setoid

specializes relation #

def specializes {X : Type u_1} [topological_space X] (x y : 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.

Equations
theorem specializes_tfae {X : Type u_1} [topological_space X] (x y : X) :
[x y, has_pure.pure x nhds y, (s : set X), is_open s y s x s, (s : set X), is_closed s x s y s, y closure {x}, closure {y} closure {x}, cluster_pt y (has_pure.pure x)].tfae

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

theorem specializes_iff_nhds {X : Type u_1} [topological_space X] {x y : X} :
x y nhds x nhds y
theorem specializes_iff_pure {X : Type u_1} [topological_space X] {x y : X} :
theorem specializes.nhds_le_nhds {X : Type u_1} [topological_space X] {x y : X} :
x y nhds x nhds y

Alias of the forward direction of specializes_iff_nhds.

theorem specializes.pure_le_nhds {X : Type u_1} [topological_space X] {x y : X} :

Alias of the forward direction of specializes_iff_pure.

theorem specializes_iff_forall_open {X : Type u_1} [topological_space X] {x y : X} :
x y (s : set X), is_open s y s x s
theorem specializes.mem_open {X : Type u_1} [topological_space X] {x y : X} {s : set X} (h : x y) (hs : is_open s) (hy : y s) :
x s
theorem is_open.not_specializes {X : Type u_1} [topological_space X] {x y : X} {s : set X} (hs : is_open s) (hx : x s) (hy : y s) :
¬x y
theorem specializes_iff_forall_closed {X : Type u_1} [topological_space X] {x y : X} :
x y (s : set X), is_closed s x s y s
theorem specializes.mem_closed {X : Type u_1} [topological_space X] {x y : X} {s : set X} (h : x y) (hs : is_closed s) (hx : x s) :
y s
theorem is_closed.not_specializes {X : Type u_1} [topological_space X] {x y : X} {s : set X} (hs : is_closed s) (hx : x s) (hy : y s) :
¬x y
theorem specializes_iff_mem_closure {X : Type u_1} [topological_space X] {x y : X} :
x y y closure {x}
theorem specializes.mem_closure {X : Type u_1} [topological_space X] {x y : X} :
x y y closure {x}

Alias of the forward direction of specializes_iff_mem_closure.

theorem specializes_iff_closure_subset {X : Type u_1} [topological_space X] {x y : X} :
x y closure {y} closure {x}
theorem specializes.closure_subset {X : Type u_1} [topological_space X] {x y : X} :
x y closure {y} closure {x}

Alias of the forward direction of specializes_iff_closure_subset.

theorem filter.has_basis.specializes_iff {X : Type u_1} [topological_space X] {x y : X} {ι : Sort u_2} {p : ι Prop} {s : ι set X} (h : (nhds y).has_basis p s) :
x y (i : ι), p i x s i
theorem specializes_rfl {X : Type u_1} [topological_space X] {x : X} :
x x
@[refl]
theorem specializes_refl {X : Type u_1} [topological_space X] (x : X) :
x x
@[trans]
theorem specializes.trans {X : Type u_1} [topological_space X] {x y z : X} :
x y y z x z
theorem specializes_of_eq {X : Type u_1} [topological_space X] {x y : X} (e : x = y) :
x y
theorem specializes_of_nhds_within {X : Type u_1} [topological_space X] {x y : X} {s : set X} (h₁ : nhds_within x s nhds_within y s) (h₂ : x s) :
x y
theorem specializes.map_of_continuous_at {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {f : X Y} (h : x y) (hy : continuous_at f y) :
f x f y
theorem specializes.map {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {f : X Y} (h : x y) (hf : continuous f) :
f x f y
theorem inducing.specializes_iff {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {f : X Y} (hf : inducing f) :
f x f y x y
theorem subtype_specializes_iff {X : Type u_1} [topological_space X] {p : X Prop} (x y : subtype p) :
x y x y
@[simp]
theorem specializes_prod {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x₁ x₂ : X} {y₁ y₂ : Y} :
(x₁, y₁) (x₂, y₂) x₁ x₂ y₁ y₂
theorem specializes.prod {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x₁ x₂ : X} {y₁ y₂ : Y} (hx : x₁ x₂) (hy : y₁ y₂) :
(x₁, y₁) (x₂, y₂)
@[simp]
theorem specializes_pi {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {f g : Π (i : ι), π i} :
f g (i : ι), f i g i
theorem not_specializes_iff_exists_open {X : Type u_1} [topological_space X] {x y : X} :
¬x y (S : set X), is_open S y S x S
theorem not_specializes_iff_exists_closed {X : Type u_1} [topological_space X] {x y : X} :
¬x y (S : set X), is_closed S x S y S

Specialization forms a preorder on the topological space.

Equations
theorem continuous.specialization_monotone {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X Y} (hf : continuous f) :

A continuous function is monotone with respect to the specialization preorders on the domain and the codomain.

inseparable relation #

def inseparable {X : Type u_1} [topological_space X] (x y : X) :
Prop

Two points x and y in a topological space are inseparable if any of the following equivalent properties hold:

Equations
theorem inseparable_def {X : Type u_1} [topological_space X] {x y : X} :
theorem inseparable_iff_specializes_and {X : Type u_1} [topological_space X] {x y : X} :
inseparable x y x y y x
theorem inseparable.specializes {X : Type u_1} [topological_space X] {x y : X} (h : inseparable x y) :
x y
theorem inseparable.specializes' {X : Type u_1} [topological_space X] {x y : X} (h : inseparable x y) :
y x
theorem specializes.antisymm {X : Type u_1} [topological_space X] {x y : X} (h₁ : x y) (h₂ : y x) :
theorem inseparable_iff_forall_open {X : Type u_1} [topological_space X] {x y : X} :
inseparable x y (s : set X), is_open s (x s y s)
theorem not_inseparable_iff_exists_open {X : Type u_1} [topological_space X] {x y : X} :
¬inseparable x y (s : set X), is_open s xor (x s) (y s)
theorem inseparable_iff_forall_closed {X : Type u_1} [topological_space X] {x y : X} :
inseparable x y (s : set X), is_closed s (x s y s)
theorem inseparable_iff_mem_closure {X : Type u_1} [topological_space X] {x y : X} :
theorem inseparable_iff_closure_eq {X : Type u_1} [topological_space X] {x y : X} :
theorem inseparable_of_nhds_within_eq {X : Type u_1} [topological_space X] {x y : X} {s : set X} (hx : x s) (hy : y s) (h : nhds_within x s = nhds_within y s) :
theorem inducing.inseparable_iff {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {f : X Y} (hf : inducing f) :
inseparable (f x) (f y) inseparable x y
theorem subtype_inseparable_iff {X : Type u_1} [topological_space X] {p : X Prop} (x y : subtype p) :
@[simp]
theorem inseparable_prod {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x₁ x₂ : X} {y₁ y₂ : Y} :
inseparable (x₁, y₁) (x₂, y₂) inseparable x₁ x₂ inseparable y₁ y₂
theorem inseparable.prod {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x₁ x₂ : X} {y₁ y₂ : Y} (hx : inseparable x₁ x₂) (hy : inseparable y₁ y₂) :
inseparable (x₁, y₁) (x₂, y₂)
@[simp]
theorem inseparable_pi {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {f g : Π (i : ι), π i} :
inseparable f g (i : ι), inseparable (f i) (g i)
@[refl]
theorem inseparable.refl {X : Type u_1} [topological_space X] (x : X) :
theorem inseparable.rfl {X : Type u_1} [topological_space X] {x : X} :
theorem inseparable.of_eq {X : Type u_1} [topological_space X] {x y : X} (e : x = y) :
@[symm]
theorem inseparable.symm {X : Type u_1} [topological_space X] {x y : X} (h : inseparable x y) :
@[trans]
theorem inseparable.trans {X : Type u_1} [topological_space X] {x y z : X} (h₁ : inseparable x y) (h₂ : inseparable y z) :
theorem inseparable.nhds_eq {X : Type u_1} [topological_space X] {x y : X} (h : inseparable x y) :
nhds x = nhds y
theorem inseparable.mem_open_iff {X : Type u_1} [topological_space X] {x y : X} {s : set X} (h : inseparable x y) (hs : is_open s) :
x s y s
theorem inseparable.mem_closed_iff {X : Type u_1} [topological_space X] {x y : X} {s : set X} (h : inseparable x y) (hs : is_closed s) :
x s y s
theorem inseparable.map_of_continuous_at {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {f : X Y} (h : inseparable x y) (hx : continuous_at f x) (hy : continuous_at f y) :
inseparable (f x) (f y)
theorem inseparable.map {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {x y : X} {f : X Y} (h : inseparable x y) (hf : continuous f) :
inseparable (f x) (f y)
theorem is_closed.not_inseparable {X : Type u_1} [topological_space X] {x y : X} {s : set X} (hs : is_closed s) (hx : x s) (hy : y s) :
theorem is_open.not_inseparable {X : Type u_1} [topological_space X] {x y : X} {s : set X} (hs : is_open s) (hx : x s) (hy : y s) :

Separation quotient #

In this section we define the quotient of a topological space by the inseparable relation.

A setoid version of inseparable, used to define the separation_quotient.

Equations

The natural map from a topological space to its separation quotient.

Equations
@[protected, instance]
def separation_quotient.lift {X : Type u_1} {α : Type u_4} [topological_space X] (f : X α) (hf : (x y : X), inseparable x y f x = f y) :

Lift a map f : X → α such that inseparable x y → f x = f y to a map separation_quotient X → α.

Equations
@[simp]
theorem separation_quotient.lift_mk {X : Type u_1} {α : Type u_4} [topological_space X] {f : X α} (hf : (x y : X), inseparable x y f x = f y) (x : X) :
@[simp]
theorem separation_quotient.lift_comp_mk {X : Type u_1} {α : Type u_4} [topological_space X] {f : X α} (hf : (x y : X), inseparable x y f x = f y) :
@[simp]
theorem separation_quotient.tendsto_lift_nhds_mk {X : Type u_1} {α : Type u_4} [topological_space X] {f : X α} {hf : (x y : X), inseparable x y f x = f y} {x : X} {l : filter α} :
@[simp]
theorem separation_quotient.continuous_at_lift {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X Y} {hf : (x y : X), inseparable x y f x = f y} {x : X} :
@[simp]
theorem separation_quotient.continuous_lift {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X Y} {hf : (x y : X), inseparable x y f x = f y} :
def separation_quotient.lift₂ {X : Type u_1} {Y : Type u_2} {α : Type u_4} [topological_space X] [topological_space Y] (f : X Y α) (hf : (a : X) (b : Y) (c : X) (d : Y), inseparable a c inseparable b d f a b = f c d) :

Lift a map f : X → Y → α such that inseparable a b → inseparable c d → f a c = f b d to a map separation_quotient X → separation_quotient Y → α.

Equations
@[simp]
theorem separation_quotient.lift₂_mk {X : Type u_1} {Y : Type u_2} {α : Type u_4} [topological_space X] [topological_space Y] {f : X Y α} (hf : (a : X) (b : Y) (c : X) (d : Y), inseparable a c inseparable b d f a b = f c d) (x : X) (y : Y) :
@[simp]
theorem separation_quotient.tendsto_lift₂_nhds {X : Type u_1} {Y : Type u_2} {α : Type u_4} [topological_space X] [topological_space Y] {f : X Y α} {hf : (a : X) (b : Y) (c : X) (d : Y), inseparable a c inseparable b d f a b = f c d} {x : X} {y : Y} {l : filter α} :
@[simp]
theorem separation_quotient.continuous_at_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [topological_space X] [topological_space Y] [topological_space Z] {f : X Y Z} {hf : (a : X) (b : Y) (c : X) (d : Y), inseparable a c inseparable b d f a b = f c d} {x : X} {y : Y} :
@[simp]
theorem separation_quotient.continuous_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [topological_space X] [topological_space Y] [topological_space Z] {f : X Y Z} {hf : (a : X) (b : Y) (c : X) (d : Y), inseparable a c inseparable b d f a b = f c d} :