Commit 2023-05-01 01:58 6d2b39cb

View on Github →

feat: port Topology.Category.Profinite.Basic (#3705)

Estimated changes

Modified Mathlib.lean

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

added def CompHaus.toProfinite

added def CompHaus.toProfiniteObj

added theorem CompHaus.toProfinite_obj'

added def FintypeCat.botTopology

added theorem FintypeCat.discreteTopology

added def FintypeCat.toProfinite

added theorem Profinite.coe_comp

added theorem Profinite.coe_id

added theorem Profinite.epi_iff_surjective

added theorem Profinite.forget_ContinuousMap_mk

added def Profinite.homeoOfIso

added theorem Profinite.isClosedMap

added theorem Profinite.isIso_of_bijective

added def Profinite.isoEquivHomeo

added def Profinite.isoOfHomeo

added def Profinite.limitCone

added def Profinite.limitConeIsLimit

added theorem Profinite.mono_iff_injective

added def Profinite.of

added def Profinite.toCompHausEquivalence

added def Profinite.toProfiniteAdjToCompHaus

added def Profinite.toTopCat

added theorem Profinite.to_compHausToTopCat

added structure Profinite

added def profiniteToCompHaus