Evaluating homeomorphisms between quotient spaces

This file records how Mathlib's Homeomorph.Quotient.congr and Homeomorph.Quotient.congrRight, homeomorphisms between quotient spaces, act on equivalence classes.

Main results

• Homeomorph.Quotient.congr_mk: congr sends the class of x to the class of its image.
• Homeomorph.Quotient.congrRight_mk: congrRight sends the class of x to the class of x.

@[simp]

theorem Homeomorph.Quotient.congr_mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {rX : Setoid X} {rY : Setoid Y} (e : X ≃ₜ Y) (h : ∀ (x₁ x₂ : X), rX x₁ x₂ ↔ rY (e x₁) (e x₂)) (x : X) : (Quotient.congr e h) ⟦x⟧ = ⟦e x⟧

Homeomorph.Quotient.congr sends the class of x to the class of its image. This is the homeomorphism counterpart of Mathlib's Quotient.congr_mk, and holds by definition for the same reason. The counterpart is needed because a homeomorphism and its underlying equivalence are applied through different coercions, so Quotient.congr_mk does not rewrite a goal stated for Homeomorph.Quotient.congr, just as Quot.congr_mk does not rewrite one stated for Quotient.congr.

@[simp]

theorem Homeomorph.Quotient.congrRight_mk {X : Type u_1} [TopologicalSpace X] {r r' : Setoid X} (h : ∀ (x₁ x₂ : X), r x₁ x₂ ↔ r' x₁ x₂) (x : X) : (Quotient.congrRight h) ⟦x⟧ = ⟦x⟧

Homeomorph.Quotient.congrRight sends the class of x to the class of x. This is the homeomorphism counterpart of Mathlib's Quot.congr_mk, and holds by definition for the same reason: Homeomorph.Quotient.congrRight is Quot.congr for the identity equivalence.