Theoremsrefl_toOpenPartialHomeomorph, refl_toPartialHomeomorph, symm_toOpenPartialHomeomorph, symm_toPartialHomeomorph, eqOn, restr, source_eq, symm', symm_eqOn_target, target_eq, apply_mem_iff, closure, compl, diff, frontier, iff_preimage_eq, iff_preimage_eq', iff_symm_preimage_eq, iff_symm_preimage_eq', image_eq, inter, inter_eq_of_inter_eq_of_eqOn, interior, isOpen_iff, leftInvOn_piecewise, map_nhdsWithin_eq, mapsTo, of_image_eq, of_preimage_eq, of_preimage_eq', of_symm_image_eq, of_symm_preimage_eq, of_symm_preimage_eq', preimage_eq, preimage_eq', restr_apply, restr_symm_apply, restr_toPartialEquiv, symm_apply_mem_iff, symm_eqOn_of_inter_eq_of_eqOn, symm_iff, symm_image_eq, symm_mapsTo, symm_preimage_eq, symm_preimage_eq', toPartialEquiv, union, restr_eqOn_source, coe_restrOpen, coe_restrOpen_symm, eqOnSource_iff, eqOnSource_refl, eq_of_eqOnSource_univ, isImage_source_target, isImage_source_target_of_disjoint, ofSet_apply, ofSet_source, ofSet_symm, ofSet_target, ofSet_toPartialEquiv, ofSet_univ_eq_refl, preimage_closure, preimage_frontier, preimage_interior, restrOpen_source, restrOpen_toPartialEquiv, restr_apply, restr_eqOnSource_restr, restr_eq_of_source_subset, restr_inter_source, restr_source, restr_source', restr_source_inter, restr_symm_apply, restr_target, restr_toPartialEquiv, restr_toPartialEquiv', restr_univ | 78 |