Commit 2023-04-27 23:18 a033eb9a

View on Github →

feat: Port Topology.Category.CompHaus.Basic (#3688) Relatively straightforward port.

Estimated changes

Modified Mathlib.lean

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

added theorem CompHaus.coe_of

added theorem CompHaus.epi_iff_surjective

added theorem CompHaus.isClosedMap

added theorem CompHaus.isIso_of_bijective

added def CompHaus.limitCone

added def CompHaus.limitConeIsLimit

added theorem CompHaus.mono_iff_injective

added def CompHaus.of

added structure CompHaus

added def compHausToTop

added def stoneCechObj

added theorem topToCompHaus_obj