Theorem SSet.Finite.exists_epi_from_isCardinalPresentable

Modification history

2026-01-04 10:53
Mathlib/AlgebraicTopology/SimplicialSet/Presentable.lean
feat(AlgebraicTopology): finite simplicial sets are `ℵ₀`-presentable (#32266) …
Added SSet.Finite.exists_epi_from_isCardinalPresentableView on Github →