Commit 2024-05-12 12:47 26781d58
View on Github →feat(LightProfinite): LightProfinite is precoherent (#11585)
This PR gives the characterisation effective epi \iff epi \iff continuous surjection in LightProfinite, following the same approach as for CompHaus, Profinite and Stonean. We conclude that LightProfinite is preregular and finitary extensive, hence precoherent, allowing the definition of light condensed sets (done in #11586).