English
A homeomorphism h: X ≃ₜ Y induces a homeomorphism between subtypes p and q whenever p = q ∘ h.
Русский
Гомеоморфизм h порождает гомеоморфизм между подтипами p и q при условии p = q ∘ h.
LaTeX
$$${\\;}{\\text{subtype}}(h, h\\_iff): {x\\#\\, p(x)} \\simeqₜ {y\\#\\, q(y)}$$$
Lean4
/-- A homeomorphism `h : X ≃ₜ Y` lifts to a homeomorphism between subtypes corresponding to
predicates `p : X → Prop` and `q : Y → Prop` so long as `p = q ∘ h`. -/
@[simps!]
def subtype {p : X → Prop} {q : Y → Prop} (h : X ≃ₜ Y) (h_iff : ∀ x, p x ↔ q (h x)) : { x // p x } ≃ₜ { y // q y }
where
continuous_toFun := by simpa [Equiv.coe_subtypeEquiv_eq_map] using h.continuous.subtype_map _
continuous_invFun := by simpa [Equiv.coe_subtypeEquiv_eq_map] using h.symm.continuous.subtype_map _
__ := h.subtypeEquiv h_iff
