Inseparable points in a topological space #

theorem specializes_TFAE {X : Type u_1} [TopologicalSpace X] (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.

theorem specializes_iff_nhds {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :

x ⤳ y ↔ nhds x ≤ nhds y

theorem Specializes.not_disjoint {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (h : x ⤳ y) :

¬Disjoint (nhds x) (nhds y)

theorem specializes_iff_pure {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :

x ⤳ y ↔ pure x ≤ nhds y

theorem Specializes.nhds_le_nhds {X : Type u_1} [TopologicalSpace X] {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} [TopologicalSpace X] {x : X} {y : X} :

x ⤳ y → pure x ≤ nhds y

Alias of the forward direction of specializes_iff_pure.

theorem ker_nhds_eq_specializes {X : Type u_1} [TopologicalSpace X] {x : X} :

(nhds x).ker = {y : X | y ⤳ x}

theorem specializes_iff_forall_open {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :

x ⤳ y ↔ ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s

theorem Specializes.mem_open {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {s : Set X} (h : x ⤳ y) (hs : IsOpen s) (hy : y ∈ s) :

x ∈ s

theorem IsOpen.not_specializes {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {s : Set X} (hs : IsOpen s) (hx : x ∉ s) (hy : y ∈ s) :

¬x ⤳ y

theorem specializes_iff_forall_closed {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :

x ⤳ y ↔ ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s

theorem Specializes.mem_closed {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {s : Set X} (h : x ⤳ y) (hs : IsClosed s) (hx : x ∈ s) :

y ∈ s

theorem IsClosed.not_specializes {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {s : Set X} (hs : IsClosed s) (hx : x ∈ s) (hy : y ∉ s) :

¬x ⤳ y

theorem specializes_iff_mem_closure {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :

x ⤳ y ↔ y ∈ closure {x}

theorem Specializes.mem_closure {X : Type u_1} [TopologicalSpace X] {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} [TopologicalSpace X] {x : X} {y : X} :

x ⤳ y ↔ closure {y} ⊆ closure {x}

theorem Specializes.closure_subset {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :

x ⤳ y → closure {y} ⊆ closure {x}

Alias of the forward direction of specializes_iff_closure_subset.

theorem specializes_iff_clusterPt {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :

x ⤳ y ↔ ClusterPt y (pure x)

theorem Filter.HasBasis.specializes_iff {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {ι : Sort u_7} {p : ι → Prop} {s : ι → Set X} (h : (nhds y).HasBasis p s) :

x ⤳ y ↔ ∀ (i : ι), p i → x ∈ s i

theorem specializes_rfl {X : Type u_1} [TopologicalSpace X] {x : X} :

x ⤳ x

theorem specializes_refl {X : Type u_1} [TopologicalSpace X] (x : X) :

x ⤳ x

theorem Specializes.trans {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {z : X} :

x ⤳ y → y ⤳ z → x ⤳ z

theorem specializes_of_eq {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (e : x = y) :

x ⤳ y

theorem Specializes.of_eq {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (e : x = y) :

x ⤳ y

Alias of specializes_of_eq.

theorem specializes_of_nhdsWithin {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {s : Set X} (h₁ : nhdsWithin x s ≤ nhdsWithin y s) (h₂ : x ∈ s) :

x ⤳ y

theorem Specializes.map_of_continuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} {f : X → Y} (h : x ⤳ y) (hy : ContinuousAt f y) :

f x ⤳ f y

theorem Specializes.map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} {f : X → Y} (h : x ⤳ y) (hf : Continuous f) :

f x ⤳ f y

theorem IsInducing.specializes_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} {f : X → Y} (hf : IsInducing f) :

f x ⤳ f y ↔ x ⤳ y

@[deprecated IsInducing.specializes_iff]

theorem Inducing.specializes_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} {f : X → Y} (hf : IsInducing f) :

f x ⤳ f y ↔ x ⤳ y

Alias of IsInducing.specializes_iff.

theorem subtype_specializes_iff {X : Type u_1} [TopologicalSpace X] {p : X → Prop} (x : Subtype p) (y : Subtype p) :

x ⤳ y ↔ ↑x ⤳ ↑y

@[simp]

theorem specializes_prod {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x₁ : X} {x₂ : X} {y₁ : Y} {y₂ : Y} :

(x₁, y₁) ⤳ (x₂, y₂) ↔ x₁ ⤳ x₂ ∧ y₁ ⤳ y₂

theorem Specializes.prod {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x₁ : X} {x₂ : X} {y₁ : Y} {y₂ : Y} (hx : x₁ ⤳ x₂) (hy : y₁ ⤳ y₂) :

(x₁, y₁) ⤳ (x₂, y₂)

theorem Specializes.fst {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {a : X × Y} {b : X × Y} (h : a ⤳ b) :

a.1 ⤳ b.1

theorem Specializes.snd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {a : X × Y} {b : X × Y} (h : a ⤳ b) :

a.2 ⤳ b.2

@[simp]

theorem specializes_pi {ι : Type u_5} {π : ι → Type u_6} [(i : ι) → TopologicalSpace (π i)] {f : (i : ι) → π i} {g : (i : ι) → π i} :

f ⤳ g ↔ ∀ (i : ι), f i ⤳ g i

theorem not_specializes_iff_exists_open {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :

¬x ⤳ y ↔ ∃ (S : Set X), IsOpen S ∧ y ∈ S ∧ x ∉ S

theorem not_specializes_iff_exists_closed {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :

¬x ⤳ y ↔ ∃ (S : Set X), IsClosed S ∧ x ∈ S ∧ y ∉ S

theorem IsOpen.continuous_piecewise_of_specializes {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} {g : X → Y} [DecidablePred fun (x : X) => x ∈ s] (hs : IsOpen s) (hf : Continuous f) (hg : Continuous g) (hspec : ∀ (x : X), f x ⤳ g x) :

Continuous (s.piecewise f g)

theorem IsClosed.continuous_piecewise_of_specializes {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} {g : X → Y} [DecidablePred fun (x : X) => x ∈ s] (hs : IsClosed s) (hf : Continuous f) (hg : Continuous g) (hspec : ∀ (x : X), g x ⤳ f x) :

Continuous (s.piecewise f g)

theorem Continuous.specialization_monotone {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) :

Monotone f

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

theorem closure_singleton_eq_Iic {X : Type u_1} [TopologicalSpace X] (x : X) :

closure {x} = Set.Iic x

def StableUnderSpecialization {X : Type u_1} [TopologicalSpace X] (s : Set X) :

A subset S of a topological space is stable under specialization if x ∈ S → y ∈ S for all x ⤳ y.

Equations

StableUnderSpecialization s = ∀ ⦃x y : X⦄, x ⤳ y → x ∈ s → y ∈ s

Instances For

def StableUnderGeneralization {X : Type u_1} [TopologicalSpace X] (s : Set X) :

A subset S of a topological space is stable under specialization if x ∈ S → y ∈ S for all y ⤳ x.

Equations

StableUnderGeneralization s = ∀ ⦃x y : X⦄, y ⤳ x → x ∈ s → y ∈ s

Instances For

StableUnderSpecialization s

theorem IsClosed.stableUnderSpecialization {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) :

StableUnderGeneralization s

theorem IsOpen.stableUnderGeneralization {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) :

StableUnderSpecialization sᶜ ↔ StableUnderGeneralization s

@[simp]

theorem stableUnderSpecialization_compl_iff {X : Type u_1} [TopologicalSpace X] {s : Set X} :

StableUnderGeneralization sᶜ ↔ StableUnderSpecialization s

@[simp]

theorem stableUnderGeneralization_compl_iff {X : Type u_1} [TopologicalSpace X] {s : Set X} :

theorem StableUnderGeneralization.compl {X : Type u_1} [TopologicalSpace X] {s : Set X} :

StableUnderGeneralization s → StableUnderSpecialization sᶜ

Alias of the reverse direction of stableUnderSpecialization_compl_iff.

theorem StableUnderSpecialization.compl {X : Type u_1} [TopologicalSpace X] {s : Set X} :

StableUnderSpecialization s → StableUnderGeneralization sᶜ

Alias of the reverse direction of stableUnderGeneralization_compl_iff.

theorem stableUnderSpecialization_univ {X : Type u_1} [TopologicalSpace X] :

StableUnderSpecialization Set.univ

StableUnderSpecialization ∅

theorem stableUnderSpecialization_empty {X : Type u_1} [TopologicalSpace X] :

theorem stableUnderGeneralization_univ {X : Type u_1} [TopologicalSpace X] :

StableUnderGeneralization Set.univ

StableUnderGeneralization ∅

theorem stableUnderGeneralization_empty {X : Type u_1} [TopologicalSpace X] :

theorem stableUnderSpecialization_sUnion {X : Type u_1} [TopologicalSpace X] (S : Set (Set X)) (H : ∀ s ∈ S, StableUnderSpecialization s) :

StableUnderSpecialization (⋃₀ S)

theorem stableUnderSpecialization_sInter {X : Type u_1} [TopologicalSpace X] (S : Set (Set X)) (H : ∀ s ∈ S, StableUnderSpecialization s) :

StableUnderSpecialization (⋂₀ S)

theorem stableUnderGeneralization_sUnion {X : Type u_1} [TopologicalSpace X] (S : Set (Set X)) (H : ∀ s ∈ S, StableUnderGeneralization s) :

StableUnderGeneralization (⋃₀ S)

theorem stableUnderGeneralization_sInter {X : Type u_1} [TopologicalSpace X] (S : Set (Set X)) (H : ∀ s ∈ S, StableUnderGeneralization s) :

StableUnderGeneralization (⋂₀ S)

theorem stableUnderSpecialization_iUnion {X : Type u_1} [TopologicalSpace X] {ι : Sort u_7} (S : ι → Set X) (H : ∀ (i : ι), StableUnderSpecialization (S i)) :

StableUnderSpecialization (⋃ (i : ι), S i)

theorem stableUnderSpecialization_iInter {X : Type u_1} [TopologicalSpace X] {ι : Sort u_7} (S : ι → Set X) (H : ∀ (i : ι), StableUnderSpecialization (S i)) :

StableUnderSpecialization (⋂ (i : ι), S i)

theorem stableUnderGeneralization_iUnion {X : Type u_1} [TopologicalSpace X] {ι : Sort u_7} (S : ι → Set X) (H : ∀ (i : ι), StableUnderGeneralization (S i)) :

StableUnderGeneralization (⋃ (i : ι), S i)

theorem stableUnderGeneralization_iInter {X : Type u_1} [TopologicalSpace X] {ι : Sort u_7} (S : ι → Set X) (H : ∀ (i : ι), StableUnderGeneralization (S i)) :

StableUnderGeneralization (⋂ (i : ι), S i)

theorem Union_closure_singleton_eq_iff {X : Type u_1} [TopologicalSpace X] {s : Set X} :

⋃ x ∈ s, closure {x} = s ↔ StableUnderSpecialization s

theorem stableUnderSpecialization_iff_Union_eq {X : Type u_1} [TopologicalSpace X] {s : Set X} :

StableUnderSpecialization s ↔ ⋃ x ∈ s, closure {x} = s

theorem StableUnderSpecialization.Union_eq {X : Type u_1} [TopologicalSpace X] {s : Set X} :

StableUnderSpecialization s → ⋃ x ∈ s, closure {x} = s

Alias of the forward direction of stableUnderSpecialization_iff_Union_eq.

theorem stableUnderSpecialization_iff_exists_sUnion_eq {X : Type u_1} [TopologicalSpace X] {s : Set X} :

StableUnderSpecialization s ↔ ∃ (S : Set (Set X)), (∀ s ∈ S, IsClosed s) ∧ ⋃₀ S = s

A set is stable under specialization iff it is a union of closed sets.

theorem stableUnderGeneralization_iff_exists_sInter_eq {X : Type u_1} [TopologicalSpace X] {s : Set X} :

StableUnderGeneralization s ↔ ∃ (S : Set (Set X)), (∀ s ∈ S, IsOpen s) ∧ ⋂₀ S = s

A set is stable under generalization iff it is an intersection of open sets.

theorem StableUnderSpecialization.preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set Y} (hs : StableUnderSpecialization s) (hf : Continuous f) :

StableUnderSpecialization (f ⁻¹' s)

theorem StableUnderGeneralization.preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set Y} (hs : StableUnderGeneralization s) (hf : Continuous f) :

StableUnderGeneralization (f ⁻¹' s)

def SpecializingMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) :

A map f between topological spaces is specializing if specializations lifts along f, i.e. for each f x' ⤳ y there is some x with x' ⤳ x whose image is y.

Equations

SpecializingMap f = Relation.Fibration (flip fun (x1 x2 : X) => x1 ⤳ x2) (flip fun (x1 x2 : Y) => x1 ⤳ x2) f

Instances For

def GeneralizingMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) :

A map f between topological spaces is generalizing if generalizations lifts along f, i.e. for each y ⤳ f x' there is some x ⤳ x' whose image is y.

Equations

GeneralizingMap f = Relation.Fibration (fun (x1 x2 : X) => x1 ⤳ x2) (fun (x1 x2 : Y) => x1 ⤳ x2) f

Instances For

theorem specializingMap_iff_closure_singleton_subset {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} :

SpecializingMap f ↔ ∀ (x : X), closure {f x} ⊆ f '' closure {x}

theorem SpecializingMap.closure_singleton_subset {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} :

SpecializingMap f → ∀ (x : X), closure {f x} ⊆ f '' closure {x}

Alias of the forward direction of specializingMap_iff_closure_singleton_subset.

theorem SpecializingMap.stableUnderSpecialization_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : SpecializingMap f) {s : Set X} (hs : StableUnderSpecialization s) :

StableUnderSpecialization (f '' s)

theorem StableUnderSpecialization.image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : SpecializingMap f) {s : Set X} (hs : StableUnderSpecialization s) :

StableUnderSpecialization (f '' s)

Alias of SpecializingMap.stableUnderSpecialization_image.

theorem specializingMap_iff_stableUnderSpecialization_image_singleton {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} :

SpecializingMap f ↔ ∀ (x : X), StableUnderSpecialization (f '' closure {x})

theorem specializingMap_iff_stableUnderSpecialization_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} :

SpecializingMap f ↔ ∀ (s : Set X), StableUnderSpecialization s → StableUnderSpecialization (f '' s)

theorem specializingMap_iff_closure_singleton {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) :

SpecializingMap f ↔ ∀ (x : X), f '' closure {x} = closure {f x}

theorem specializingMap_iff_isClosed_image_closure_singleton {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) :

SpecializingMap f ↔ ∀ (x : X), IsClosed (f '' closure {x})

theorem IsClosedMap.specializingMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsClosedMap f) :

SpecializingMap f

theorem IsInducing.specializingMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsInducing f) (h : StableUnderSpecialization (Set.range f)) :

SpecializingMap f

@[deprecated IsInducing.specializingMap]

theorem Inducing.specializingMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsInducing f) (h : StableUnderSpecialization (Set.range f)) :

SpecializingMap f

Alias of IsInducing.specializingMap.

theorem IsInducing.generalizingMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsInducing f) (h : StableUnderGeneralization (Set.range f)) :

@[deprecated IsInducing.generalizingMap]

theorem Inducing.generalizingMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsInducing f) (h : StableUnderGeneralization (Set.range f)) :

Alias of IsInducing.generalizingMap.

theorem IsOpenEmbedding.generalizingMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsOpenEmbedding f) :

@[deprecated IsOpenEmbedding.generalizingMap]

theorem OpenEmbedding.generalizingMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsOpenEmbedding f) :

Alias of IsOpenEmbedding.generalizingMap.

theorem SpecializingMap.stableUnderSpecialization_range {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (h : SpecializingMap f) :

StableUnderSpecialization (Set.range f)

theorem GeneralizingMap.stableUnderGeneralization_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : GeneralizingMap f) {s : Set X} (hs : StableUnderGeneralization s) :

StableUnderGeneralization (f '' s)

theorem GeneralizingMap_iff_stableUnderGeneralization_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} :

GeneralizingMap f ↔ ∀ (s : Set X), StableUnderGeneralization s → StableUnderGeneralization (f '' s)

theorem StableUnderGeneralization.image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : GeneralizingMap f) {s : Set X} (hs : StableUnderGeneralization s) :

StableUnderGeneralization (f '' s)

Alias of GeneralizingMap.stableUnderGeneralization_image.

theorem GeneralizingMap.stableUnderGeneralization_range {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (h : GeneralizingMap f) :

StableUnderGeneralization (Set.range f)

`Inseparable` relation #

theorem inseparable_def {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :

Inseparable x y ↔ nhds x = nhds y

theorem inseparable_iff_specializes_and {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :

Inseparable x y ↔ x ⤳ y ∧ y ⤳ x

theorem Inseparable.specializes {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (h : Inseparable x y) :

x ⤳ y

theorem Inseparable.specializes' {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (h : Inseparable x y) :

y ⤳ x

theorem Specializes.antisymm {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (h₁ : x ⤳ y) (h₂ : y ⤳ x) :

Inseparable x y

theorem inseparable_iff_forall_open {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :

Inseparable x y ↔ ∀ (s : Set X), IsOpen s → (x ∈ s ↔ y ∈ s)

theorem not_inseparable_iff_exists_open {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :

¬Inseparable x y ↔ ∃ (s : Set X), IsOpen s ∧ Xor' (x ∈ s) (y ∈ s)

theorem inseparable_iff_forall_closed {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :

Inseparable x y ↔ ∀ (s : Set X), IsClosed s → (x ∈ s ↔ y ∈ s)

theorem inseparable_iff_mem_closure {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :

Inseparable x y ↔ x ∈ closure {y} ∧ y ∈ closure {x}

theorem inseparable_iff_closure_eq {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :

Inseparable x y ↔ closure {x} = closure {y}

theorem inseparable_of_nhdsWithin_eq {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {s : Set X} (hx : x ∈ s) (hy : y ∈ s) (h : nhdsWithin x s = nhdsWithin y s) :

Inseparable x y

theorem IsInducing.inseparable_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} {f : X → Y} (hf : IsInducing f) :

Inseparable (f x) (f y) ↔ Inseparable x y

@[deprecated IsInducing.inseparable_iff]

theorem Inducing.inseparable_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} {f : X → Y} (hf : IsInducing f) :

Inseparable (f x) (f y) ↔ Inseparable x y

Alias of IsInducing.inseparable_iff.

theorem subtype_inseparable_iff {X : Type u_1} [TopologicalSpace X] {p : X → Prop} (x : Subtype p) (y : Subtype p) :

Inseparable x y ↔ Inseparable ↑x ↑y

@[simp]

theorem inseparable_prod {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x₁ : X} {x₂ : X} {y₁ : 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} [TopologicalSpace X] [TopologicalSpace Y] {x₁ : X} {x₂ : X} {y₁ : 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 : ι) → TopologicalSpace (π i)] {f : (i : ι) → π i} {g : (i : ι) → π i} :

Inseparable f g ↔ ∀ (i : ι), Inseparable (f i) (g i)

theorem Inseparable.refl {X : Type u_1} [TopologicalSpace X] (x : X) :

Inseparable x x

theorem Inseparable.rfl {X : Type u_1} [TopologicalSpace X] {x : X} :

Inseparable x x

theorem Inseparable.of_eq {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (e : x = y) :

Inseparable x y

theorem Inseparable.symm {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (h : Inseparable x y) :

Inseparable y x

theorem Inseparable.trans {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {z : X} (h₁ : Inseparable x y) (h₂ : Inseparable y z) :

Inseparable x z

theorem Inseparable.nhds_eq {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (h : Inseparable x y) :

nhds x = nhds y

theorem Inseparable.mem_open_iff {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {s : Set X} (h : Inseparable x y) (hs : IsOpen s) :

x ∈ s ↔ y ∈ s

theorem Inseparable.mem_closed_iff {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {s : Set X} (h : Inseparable x y) (hs : IsClosed s) :

x ∈ s ↔ y ∈ s

theorem Inseparable.map_of_continuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} {f : X → Y} (h : Inseparable x y) (hx : ContinuousAt f x) (hy : ContinuousAt f y) :

Inseparable (f x) (f y)

theorem Inseparable.map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} {f : X → Y} (h : Inseparable x y) (hf : Continuous f) :

Inseparable (f x) (f y)

theorem IsClosed.not_inseparable {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {s : Set X} (hs : IsClosed s) (hx : x ∈ s) (hy : y ∉ s) :

¬Inseparable x y

theorem IsOpen.not_inseparable {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {s : Set X} (hs : IsOpen s) (hx : x ∈ s) (hy : y ∉ s) :

¬Inseparable x y

Separation quotient #

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

instance instTopologicalSpaceSeparationQuotient (X : Type u_1) [TopologicalSpace X] :

TopologicalSpace (SeparationQuotient X)

Equations

instTopologicalSpaceSeparationQuotient X = instTopologicalSpaceQuotient

def SeparationQuotient.mk {X : Type u_1} [TopologicalSpace X] :

X → SeparationQuotient X

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

Equations

SeparationQuotient.mk = Quotient.mk''

Instances For

theorem SeparationQuotient.isQuotientMap_mk {X : Type u_1} [TopologicalSpace X] :

IsQuotientMap SeparationQuotient.mk

@[deprecated SeparationQuotient.isQuotientMap_mk]

theorem SeparationQuotient.quotientMap_mk {X : Type u_1} [TopologicalSpace X] :

IsQuotientMap SeparationQuotient.mk

Alias of SeparationQuotient.isQuotientMap_mk.

theorem SeparationQuotient.continuous_mk {X : Type u_1} [TopologicalSpace X] :

Continuous SeparationQuotient.mk

@[simp]

theorem SeparationQuotient.mk_eq_mk {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :

SeparationQuotient.mk x = SeparationQuotient.mk y ↔ Inseparable x y

theorem SeparationQuotient.surjective_mk {X : Type u_1} [TopologicalSpace X] :

Function.Surjective SeparationQuotient.mk

@[simp]

theorem SeparationQuotient.range_mk {X : Type u_1} [TopologicalSpace X] :

Set.range SeparationQuotient.mk = Set.univ

instance SeparationQuotient.instNonempty {X : Type u_1} [TopologicalSpace X] [Nonempty X] :

Nonempty (SeparationQuotient X)

Equations

⋯ = ⋯

instance SeparationQuotient.instInhabited {X : Type u_1} [TopologicalSpace X] [Inhabited X] :

Inhabited (SeparationQuotient X)

Equations

SeparationQuotient.instInhabited = { default := SeparationQuotient.mk default }

instance SeparationQuotient.instSubsingleton {X : Type u_1} [TopologicalSpace X] [Subsingleton X] :

Subsingleton (SeparationQuotient X)

Equations

⋯ = ⋯

instance SeparationQuotient.instZero {X : Type u_1} [TopologicalSpace X] [Zero X] :

Zero (SeparationQuotient X)

Equations

SeparationQuotient.instZero = { zero := SeparationQuotient.mk 0 }

instance SeparationQuotient.instOne {X : Type u_1} [TopologicalSpace X] [One X] :

One (SeparationQuotient X)

Equations

SeparationQuotient.instOne = { one := SeparationQuotient.mk 1 }

@[simp]

theorem SeparationQuotient.mk_zero {X : Type u_1} [TopologicalSpace X] [Zero X] :

SeparationQuotient.mk 0 = 0

@[simp]

theorem SeparationQuotient.mk_one {X : Type u_1} [TopologicalSpace X] [One X] :

SeparationQuotient.mk 1 = 1

theorem SeparationQuotient.preimage_image_mk_open {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsOpen s) :

SeparationQuotient.mk ⁻¹' (SeparationQuotient.mk '' s) = s

theorem SeparationQuotient.isOpenMap_mk {X : Type u_1} [TopologicalSpace X] :

IsOpenMap SeparationQuotient.mk

theorem SeparationQuotient.isOpenQuotientMap_mk {X : Type u_1} [TopologicalSpace X] :

IsOpenQuotientMap SeparationQuotient.mk

theorem SeparationQuotient.preimage_image_mk_closed {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) :

SeparationQuotient.mk ⁻¹' (SeparationQuotient.mk '' s) = s

theorem SeparationQuotient.isInducing_mk {X : Type u_1} [TopologicalSpace X] :

IsInducing SeparationQuotient.mk

@[deprecated SeparationQuotient.isInducing_mk]

theorem SeparationQuotient.inducing_mk {X : Type u_1} [TopologicalSpace X] :

IsInducing SeparationQuotient.mk

Alias of SeparationQuotient.isInducing_mk.

theorem SeparationQuotient.isClosedMap_mk {X : Type u_1} [TopologicalSpace X] :

IsClosedMap SeparationQuotient.mk

@[simp]

theorem SeparationQuotient.comap_mk_nhds_mk {X : Type u_1} [TopologicalSpace X] {x : X} :

Filter.comap SeparationQuotient.mk (nhds (SeparationQuotient.mk x)) = nhds x

@[simp]

theorem SeparationQuotient.comap_mk_nhdsSet_image {X : Type u_1} [TopologicalSpace X] {s : Set X} :

Filter.comap SeparationQuotient.mk (nhdsSet (SeparationQuotient.mk '' s)) = nhdsSet s

theorem SeparationQuotient.map_mk_nhds {X : Type u_1} [TopologicalSpace X] {x : X} :

Filter.map SeparationQuotient.mk (nhds x) = nhds (SeparationQuotient.mk x)

theorem SeparationQuotient.map_mk_nhdsSet {X : Type u_1} [TopologicalSpace X] {s : Set X} :

Filter.map SeparationQuotient.mk (nhdsSet s) = nhdsSet (SeparationQuotient.mk '' s)

theorem SeparationQuotient.comap_mk_nhdsSet {X : Type u_1} [TopologicalSpace X] {t : Set (SeparationQuotient X)} :

Filter.comap SeparationQuotient.mk (nhdsSet t) = nhdsSet (SeparationQuotient.mk ⁻¹' t)

theorem SeparationQuotient.preimage_mk_closure {X : Type u_1} [TopologicalSpace X] {t : Set (SeparationQuotient X)} :

SeparationQuotient.mk ⁻¹' closure t = closure (SeparationQuotient.mk ⁻¹' t)

theorem SeparationQuotient.preimage_mk_interior {X : Type u_1} [TopologicalSpace X] {t : Set (SeparationQuotient X)} :

SeparationQuotient.mk ⁻¹' interior t = interior (SeparationQuotient.mk ⁻¹' t)

theorem SeparationQuotient.preimage_mk_frontier {X : Type u_1} [TopologicalSpace X] {t : Set (SeparationQuotient X)} :

SeparationQuotient.mk ⁻¹' frontier t = frontier (SeparationQuotient.mk ⁻¹' t)

theorem SeparationQuotient.image_mk_closure {X : Type u_1} [TopologicalSpace X] {s : Set X} :

SeparationQuotient.mk '' closure s = closure (SeparationQuotient.mk '' s)

theorem SeparationQuotient.map_prod_map_mk_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (x : X) (y : Y) :

Filter.map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (nhds (x, y)) = nhds (SeparationQuotient.mk x, SeparationQuotient.mk y)

theorem SeparationQuotient.map_mk_nhdsWithin_preimage {X : Type u_1} [TopologicalSpace X] (s : Set (SeparationQuotient X)) (x : X) :

Filter.map SeparationQuotient.mk (nhdsWithin x (SeparationQuotient.mk ⁻¹' s)) = nhdsWithin (SeparationQuotient.mk x) s

theorem SeparationQuotient.isQuotientMap_prodMap_mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :

IsQuotientMap (Prod.map SeparationQuotient.mk SeparationQuotient.mk)

The map (x, y) ↦ (mk x, mk y) is a quotient map.

@[deprecated SeparationQuotient.isQuotientMap_prodMap_mk]

theorem SeparationQuotient.quotientMap_prodMap_mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :

IsQuotientMap (Prod.map SeparationQuotient.mk SeparationQuotient.mk)

Alias of SeparationQuotient.isQuotientMap_prodMap_mk.

The map (x, y) ↦ (mk x, mk y) is a quotient map.

def SeparationQuotient.lift {X : Type u_1} {α : Type u_4} [TopologicalSpace X] (f : X → α) (hf : ∀ (x y : X), Inseparable x y → f x = f y) :

SeparationQuotient X → α

Lift a map f : X → α such that Inseparable x y → f x = f y to a map SeparationQuotient X → α.

Equations

SeparationQuotient.lift f hf x = Quotient.liftOn' x f hf

Instances For

@[simp]

theorem SeparationQuotient.lift_mk {X : Type u_1} {α : Type u_4} [TopologicalSpace X] {f : X → α} (hf : ∀ (x y : X), Inseparable x y → f x = f y) (x : X) :

SeparationQuotient.lift f hf (SeparationQuotient.mk x) = f x

@[simp]

theorem SeparationQuotient.lift_comp_mk {X : Type u_1} {α : Type u_4} [TopologicalSpace X] {f : X → α} (hf : ∀ (x y : X), Inseparable x y → f x = f y) :

SeparationQuotient.lift f hf ∘ SeparationQuotient.mk = f

@[simp]

theorem SeparationQuotient.tendsto_lift_nhds_mk {X : Type u_1} {α : Type u_4} [TopologicalSpace X] {x : X} {f : X → α} {hf : ∀ (x y : X), Inseparable x y → f x = f y} {l : Filter α} :

Filter.Tendsto (SeparationQuotient.lift f hf) (nhds (SeparationQuotient.mk x)) l ↔ Filter.Tendsto f (nhds x) l

@[simp]

theorem SeparationQuotient.tendsto_lift_nhdsWithin_mk {X : Type u_1} {α : Type u_4} [TopologicalSpace X] {x : X} {f : X → α} {hf : ∀ (x y : X), Inseparable x y → f x = f y} {s : Set (SeparationQuotient X)} {l : Filter α} :

Filter.Tendsto (SeparationQuotient.lift f hf) (nhdsWithin (SeparationQuotient.mk x) s) l ↔ Filter.Tendsto f (nhdsWithin x (SeparationQuotient.mk ⁻¹' s)) l

@[simp]

theorem SeparationQuotient.continuousAt_lift {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {f : X → Y} {hf : ∀ (x y : X), Inseparable x y → f x = f y} :

ContinuousAt (SeparationQuotient.lift f hf) (SeparationQuotient.mk x) ↔ ContinuousAt f x

@[simp]

theorem SeparationQuotient.continuousWithinAt_lift {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {f : X → Y} {hf : ∀ (x y : X), Inseparable x y → f x = f y} {s : Set (SeparationQuotient X)} :

ContinuousWithinAt (SeparationQuotient.lift f hf) s (SeparationQuotient.mk x) ↔ ContinuousWithinAt f (SeparationQuotient.mk ⁻¹' s) x

@[simp]

theorem SeparationQuotient.continuousOn_lift {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {hf : ∀ (x y : X), Inseparable x y → f x = f y} {s : Set (SeparationQuotient X)} :

ContinuousOn (SeparationQuotient.lift f hf) s ↔ ContinuousOn f (SeparationQuotient.mk ⁻¹' s)

@[simp]

theorem SeparationQuotient.continuous_lift {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {hf : ∀ (x y : X), Inseparable x y → f x = f y} :

Continuous (SeparationQuotient.lift f hf) ↔ Continuous f

def SeparationQuotient.lift₂ {X : Type u_1} {Y : Type u_2} {α : Type u_4} [TopologicalSpace X] [TopologicalSpace 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) :

SeparationQuotient X → SeparationQuotient Y → α

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

Equations

SeparationQuotient.lift₂ f hf x y = Quotient.liftOn₂' x y f hf

Instances For

@[simp]

theorem SeparationQuotient.lift₂_mk {X : Type u_1} {Y : Type u_2} {α : Type u_4} [TopologicalSpace X] [TopologicalSpace 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) :

SeparationQuotient.lift₂ f hf (SeparationQuotient.mk x) (SeparationQuotient.mk y) = f x y

@[simp]

theorem SeparationQuotient.tendsto_lift₂_nhds {X : Type u_1} {Y : Type u_2} {α : Type u_4} [TopologicalSpace X] [TopologicalSpace 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 α} :

Filter.Tendsto (Function.uncurry (SeparationQuotient.lift₂ f hf)) (nhds (SeparationQuotient.mk x, SeparationQuotient.mk y)) l ↔ Filter.Tendsto (Function.uncurry f) (nhds (x, y)) l

@[simp]

theorem SeparationQuotient.tendsto_lift₂_nhdsWithin {X : Type u_1} {Y : Type u_2} {α : Type u_4} [TopologicalSpace X] [TopologicalSpace 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} {s : Set (SeparationQuotient X × SeparationQuotient Y)} {l : Filter α} :

Filter.Tendsto (Function.uncurry (SeparationQuotient.lift₂ f hf)) (nhdsWithin (SeparationQuotient.mk x, SeparationQuotient.mk y) s) l ↔ Filter.Tendsto (Function.uncurry f) (nhdsWithin (x, y) (Prod.map SeparationQuotient.mk SeparationQuotient.mk ⁻¹' s)) l

@[simp]

theorem SeparationQuotient.continuousAt_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace 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} :

ContinuousAt (Function.uncurry (SeparationQuotient.lift₂ f hf)) (SeparationQuotient.mk x, SeparationQuotient.mk y) ↔ ContinuousAt (Function.uncurry f) (x, y)

@[simp]

theorem SeparationQuotient.continuousWithinAt_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace 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} {s : Set (SeparationQuotient X × SeparationQuotient Y)} {x : X} {y : Y} :

ContinuousWithinAt (Function.uncurry (SeparationQuotient.lift₂ f hf)) s (SeparationQuotient.mk x, SeparationQuotient.mk y) ↔ ContinuousWithinAt (Function.uncurry f) (Prod.map SeparationQuotient.mk SeparationQuotient.mk ⁻¹' s) (x, y)

@[simp]

theorem SeparationQuotient.continuousOn_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace 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} {s : Set (SeparationQuotient X × SeparationQuotient Y)} :

ContinuousOn (Function.uncurry (SeparationQuotient.lift₂ f hf)) s ↔ ContinuousOn (Function.uncurry f) (Prod.map SeparationQuotient.mk SeparationQuotient.mk ⁻¹' s)

@[simp]

theorem SeparationQuotient.continuous_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace 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} :

Continuous (Function.uncurry (SeparationQuotient.lift₂ f hf)) ↔ Continuous (Function.uncurry f)