Theorem LightProfinite.epi_iff_surjective

Modification history

2024-06-11 13:06

Mathlib/Topology/Category/LightProfinite/Basic.lean

refactor(LightProfinite): redefine light profinite spaces as second countable profinite spaces (#13319) …

Modified LightProfinite.epi_iff_surjective View on Github →

2024-05-12 12:47

Mathlib/Topology/Category/LightProfinite/EffectiveEpi.lean

feat(LightProfinite): `LightProfinite` is precoherent (#11585) …

Added LightProfinite.epi_iff_surjective View on Github →