Documentation

Mathlib.Topology.Inseparable

Inseparable points in a topological space #

In this file we prove basic properties of the following notions defined elsewhere.

We also prove various basic properties of the relation Inseparable.

Notations #

Tags #

topological space, separation setoid

Specializes relation #

theorem specializes_TFAE {X : Type u_1} [TopologicalSpace X] (x : X) (y : X) :
[x y, pure x nhds y, ∀ (s : Set X), IsOpen sy sx s, ∀ (s : Set X), IsClosed sx sy 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) :
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 ynhds 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 ypure 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 sy sx 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 : xs) (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 sx sy 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 : ys) :
¬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 yy 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 yclosure {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 ix 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 yy zx z
theorem specializes_of_eq {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (e : x = y) :
x y
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 : XY} (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 : XY} (h : x y) (hf : Continuous f) :
f x f y
theorem Inducing.specializes_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} {f : XY} (hf : Inducing f) :
f x f y x y
theorem subtype_specializes_iff {X : Type u_1} [TopologicalSpace X] {p : XProp} (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 xS
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 yS
theorem IsOpen.continuous_piecewise_of_specializes {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : XY} {g : XY} [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 : XY} {g : XY} [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 : XY} (hf : Continuous f) :

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

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

Equations
Instances For

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

    Equations
    Instances For
      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 StableUnderSpecialization.Union_eq {X : Type u_1} [TopologicalSpace X] {s : Set X} :
      StableUnderSpecialization sxs, closure {x} = s

      Alias of the forward direction of stableUnderSpecialization_iff_Union_eq.

      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)), (∀ sS, IsOpen s) ⋂₀ S = s

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

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

      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
      Instances For
        def GeneralizingMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) :

        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
        Instances For
          theorem specializingMap_iff_closure_singleton_subset {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} :
          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 : XY} :
          SpecializingMap f∀ (x : X), closure {f x} f '' closure {x}

          Alias of the forward direction of specializingMap_iff_closure_singleton_subset.

          theorem specializingMap_iff_closure_singleton {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : Continuous f) :
          SpecializingMap f ∀ (x : X), f '' closure {x} = closure {f x}
          theorem IsClosedMap.specializingMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : IsClosedMap f) :

          Inseparable relation #

          theorem inseparable_def {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :
          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) :
          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} :
          theorem inseparable_iff_closure_eq {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :
          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) :
          theorem Inducing.inseparable_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} {f : XY} (hf : Inducing f) :
          Inseparable (f x) (f y) Inseparable x y
          theorem subtype_inseparable_iff {X : Type u_1} [TopologicalSpace X] {p : XProp} (x : Subtype p) (y : Subtype p) :
          @[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) :
          theorem Inseparable.rfl {X : Type u_1} [TopologicalSpace X] {x : X} :
          theorem Inseparable.of_eq {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (e : x = y) :
          theorem Inseparable.symm {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (h : Inseparable x y) :
          theorem Inseparable.trans {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {z : X} (h₁ : Inseparable x y) (h₂ : Inseparable y 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 : XY} (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 : XY} (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 : ys) :
          theorem IsOpen.not_inseparable {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {s : Set X} (hs : IsOpen s) (hx : x s) (hy : ys) :

          Separation quotient #

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

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

          Equations
          • SeparationQuotient.mk = Quotient.mk''
          Instances For
            theorem SeparationQuotient.quotientMap_mk {X : Type u_1} [TopologicalSpace X] :
            QuotientMap SeparationQuotient.mk
            theorem SeparationQuotient.continuous_mk {X : Type u_1} [TopologicalSpace X] :
            Continuous SeparationQuotient.mk
            @[simp]
            theorem SeparationQuotient.range_mk {X : Type u_1} [TopologicalSpace X] :
            Set.range SeparationQuotient.mk = Set.univ
            Equations
            Equations
            Equations
            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.preimage_image_mk_closed {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) :
            SeparationQuotient.mk ⁻¹' (SeparationQuotient.mk '' s) = s
            theorem SeparationQuotient.inducing_mk {X : Type u_1} [TopologicalSpace X] :
            Inducing SeparationQuotient.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.quotientMap_prodMap_mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :
            QuotientMap (Prod.map SeparationQuotient.mk SeparationQuotient.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 yf x = f y) :

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

            Equations
            Instances For
              @[simp]
              theorem SeparationQuotient.lift_mk {X : Type u_1} {α : Type u_4} [TopologicalSpace X] {f : Xα} (hf : ∀ (x y : X), Inseparable x yf x = f y) (x : X) :
              @[simp]
              theorem SeparationQuotient.lift_comp_mk {X : Type u_1} {α : Type u_4} [TopologicalSpace X] {f : Xα} (hf : ∀ (x y : X), Inseparable x yf 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 yf x = f y} {l : Filter α} :
              @[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 yf x = f y} {s : Set (SeparationQuotient X)} {l : Filter α} :
              @[simp]
              theorem SeparationQuotient.continuousAt_lift {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {f : XY} {hf : ∀ (x y : X), Inseparable x yf x = f y} :
              @[simp]
              theorem SeparationQuotient.continuousWithinAt_lift {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {f : XY} {hf : ∀ (x y : X), Inseparable x yf x = f y} {s : Set (SeparationQuotient X)} :
              @[simp]
              theorem SeparationQuotient.continuousOn_lift {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {hf : ∀ (x y : X), Inseparable x yf 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 : XY} {hf : ∀ (x y : X), Inseparable x yf x = f y} :
              def SeparationQuotient.lift₂ {X : Type u_1} {Y : Type u_2} {α : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] (f : XYα) (hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a cInseparable b df 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 SeparationQuotient X → SeparationQuotient Y → α.

              Equations
              Instances For
                @[simp]
                theorem SeparationQuotient.lift₂_mk {X : Type u_1} {Y : Type u_2} {α : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] {f : XYα} (hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a cInseparable b df a b = f c d) (x : X) (y : Y) :
                @[simp]
                theorem SeparationQuotient.tendsto_lift₂_nhds {X : Type u_1} {Y : Type u_2} {α : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] {f : XYα} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a cInseparable b df a b = f c d} {x : X} {y : Y} {l : Filter α} :
                @[simp]
                theorem SeparationQuotient.tendsto_lift₂_nhdsWithin {X : Type u_1} {Y : Type u_2} {α : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] {f : XYα} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a cInseparable b df a b = f c d} {x : X} {y : Y} {s : Set (SeparationQuotient X × SeparationQuotient Y)} {l : Filter α} :
                @[simp]
                theorem SeparationQuotient.continuousAt_lift₂ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : XYZ} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a cInseparable b df a b = f c d} {x : X} {y : 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 : XYZ} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a cInseparable b df a b = f c d} {s : Set (SeparationQuotient X × SeparationQuotient Y)} {x : X} {y : 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 : XYZ} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a cInseparable b df 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 : XYZ} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a cInseparable b df a b = f c d} :
                theorem continuous_congr_of_inseparable {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {g : XY} (h : ∀ (x : X), Inseparable (f x) (g x)) :