Homeomorphisms between quotient spaces

def Homeomorph.Quot.congr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {rX : X → X → Prop} {rY : Y → Y → Prop} (e : X ≃ₜ Y) (eq : ∀ (x₁ x₂ : X), rX x₁ x₂ ↔ rY (e x₁) (e x₂)) : Quot rX ≃ₜ Quot rY

A homeomorphism e : X ≃ₜ Y generates a homeomorphism between quotient spaces, if rX x₁ x₂ ↔ rY (e x₁) (e x₂).

Equations

• Homeomorph.Quot.congr e eq = { toEquiv := Quot.congr (↑e) eq, continuous_toFun := ⋯, continuous_invFun := ⋯ }

def Homeomorph.Quot.congrRight {X : Type u_1} [TopologicalSpace X] {r r' : X → X → Prop} (eq : ∀ (x₁ x₂ : X), r x₁ x₂ ↔ r' x₁ x₂) : Quot r ≃ₜ Quot r'

Quotient spaces for equal relations are homeomorphic.

Equations

• Homeomorph.Quot.congrRight eq = Homeomorph.Quot.congr (Homeomorph.refl X) eq

def Homeomorph.Quot.congrLeft {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {r : X → X → Prop} (e : X ≃ₜ Y) : Quot r ≃ₜ Quot fun (y₁ y₂ : Y) => r (e.symm y₁) (e.symm y₂)

A homeomorphism e : X ≃ₜ Y generates an equivalence between the quotient space of X by a relation rX and the quotient space of Y by the image of this relation under e.

Equations

• Homeomorph.Quot.congrLeft e = Homeomorph.Quot.congr e ⋯

def Homeomorph.Quotient.congr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {rX : Setoid X} {rY : Setoid Y} (e : X ≃ₜ Y) (eq : ∀ (x₁ x₂ : X), rX x₁ x₂ ↔ rY (e x₁) (e x₂)) : Quotient rX ≃ₜ Quotient rY

A homeomorphism e : X ≃ₜ Y generates a homeomorphism between quotient spaces, if rX x₁ x₂ ↔ rY (e x₁) (e x₂).

Equations

• Homeomorph.Quotient.congr e eq = Homeomorph.Quot.congr e eq

def Homeomorph.Quotient.congrRight {X : Type u_1} [TopologicalSpace X] {r r' : Setoid X} (eq : ∀ (x₁ x₂ : X), r x₁ x₂ ↔ r' x₁ x₂) : Quotient r ≃ₜ Quotient r'

Quotient spaces for equal relations are homeomorphic.

Equations

• Homeomorph.Quotient.congrRight eq = Homeomorph.Quot.congrRight eq

def Homeomorph.quotientBot {X : Type u_1} [TopologicalSpace X] : Quotient ⊥ ≃ₜ X

The quotient by the trivial relation is homeomorphic to the original space.

Equations

• Homeomorph.quotientBot = { toEquiv := Setoid.quotientBotEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }