Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-16 02:20 46b3fae0

View on Github →

feat(topology/category/*/projective): CompHaus and Profinite have enough projectives (#8613)

Estimated changes

Modified docs/references.bib

Renamed src/topology/category/CompHaus.lean to src/topology/category/CompHaus/default.lean

added theorem CompHaus.epi_iff_surjective

added theorem CompHaus.mono_iff_injective

Created src/topology/category/CompHaus/projective.lean

added def CompHaus.projective_presentation

Modified src/topology/category/Profinite/default.lean

added theorem Profinite.epi_iff_surjective

added theorem Profinite.mono_iff_injective

Created src/topology/category/Profinite/projective.lean

added def Profinite.projective_presentation

Modified src/topology/homeomorph.lean

added theorem homeomorph.compact_space

added theorem homeomorph.t2_space

Modified src/topology/stone_cech.lean