Commit 2024-01-25 02:46 8c661e54

feat: add Homeomorph.subtype for lifting homeomorphisms to subtypes (#9959) This extends Equiv.subtypeEquiv, which promotes e : α ≃ β to e.subtypeEquiv _ : {a : α // p a} ≃ {b : β // q b}, to homeomorphisms. We also add a missing lemma linking Equiv.subtypeEquiv to Subtype.map, and update the definition to use Subtype.map also.