Def LightProfinite.EffectiveEpi.struct

Modification history

2024-07-31 16:34

Mathlib/Topology/Category/LightProfinite/EffectiveEpi.lean

refactor(Topology/Category): use `CompHausLike` API for limits in `LightProfinite` (#15362)

Deleted LightProfinite.EffectiveEpi.struct View on Github →

2024-05-12 12:47

Mathlib/Topology/Category/LightProfinite/EffectiveEpi.lean

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

Added LightProfinite.EffectiveEpi.struct View on Github →