Commit 2024-06-19 15:38 4dcf21f6

View on Github →

refactor(Topology/Category): add CompHausLike.Basic (#13904) This is the first part of the refactor of CompHaus and friends (adding the new API which will eventually be used to redefine the categories of compact Hausdorff spaces, see #12930)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Category/CompHausLike/Basic.lean

added theorem CompHausLike.coe_comp

added theorem CompHausLike.coe_id

added theorem CompHausLike.coe_of

added def CompHausLike.compHausLikeToTop

added theorem CompHausLike.epi_of_surjective

added def CompHausLike.fullyFaithfulCompHausLikeToTop

added def CompHausLike.fullyFaithfulToCompHausLike

added def CompHausLike.homeoOfIso

added theorem CompHausLike.isClosedMap

added theorem CompHausLike.isIso_of_bijective

added def CompHausLike.isoEquivHomeo

added def CompHausLike.isoOfHomeo

added theorem CompHausLike.mono_iff_injective

added def CompHausLike.of

added def CompHausLike.toCompHausLike

added structure CompHausLike