Commit 2023-06-08 04:21 3d02c7d5

View on Github →

feat: port Topology.Category.Compactum (#3872)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Category/Compactum.lean

added def Compactum.adj

added theorem Compactum.cl_eq_closure

added theorem Compactum.continuous_of_hom

added def Compactum.forget

added def Compactum.free

added def Compactum.homOfContinuous

added def Compactum.incl

added theorem Compactum.isClosed_cl

added theorem Compactum.isClosed_iff

added def Compactum.join

added theorem Compactum.join_distrib

added theorem Compactum.le_nhds_of_str_eq

added theorem Compactum.lim_eq_str

added def Compactum.str

added theorem Compactum.str_eq_of_le_nhds

added theorem Compactum.str_hom_commute

added theorem Compactum.str_incl

added def Compactum

added theorem compactumToCompHaus.essSurj

added theorem compactumToCompHaus.faithful

added def compactumToCompHaus.full

added def compactumToCompHaus.isoOfTopologicalSpace

added def compactumToCompHaus

added def compactumToCompHausCompForget