Theorem LightProfinite.pullback.lift_fst

Modification history

2024-07-31 16:34

Mathlib/Topology/Category/LightProfinite/Limits.lean

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

Deleted LightProfinite.pullback.lift_fst View on Github →

2024-05-07 21:46

Mathlib/Topology/Category/LightProfinite/Limits.lean

feat(LightProfinite): (co)limits (#9513) …

Added LightProfinite.pullback.lift_fst View on Github →