Evaluating the homeomorphism between equal sets

This file records how Mathlib's Homeomorph.setCongr, the homeomorphism between the subtypes of two equal sets, acts on points in both directions.

Main results

• Homeomorph.setCongr_apply: setCongr retypes a point without moving it.
• TauCeti.Homeomorph.setCongr_symm_apply: its inverse also retypes a point without moving it.

@[simp]

theorem Homeomorph.setCongr_apply {X : Type u_1} [TopologicalSpace X] {s t : Set X} (h : s = t) (x : ↑s) : (setCongr h) x = ⟨↑x, ⋯⟩

Homeomorph.setCongr retypes a point without moving it. This is the homeomorphism counterpart of Mathlib's Set.equivOfEq_apply, which does not match through the homeomorphism constructor.

@[simp]

theorem TauCeti.Homeomorph.setCongr_symm_apply {X : Type u_1} [TopologicalSpace X] {s t : Set X} (h : s = t) (x : ↑t) : (Homeomorph.setCongr h).symm x = ⟨↑x, ⋯⟩

The inverse of Homeomorph.setCongr retypes a point without moving it.