Theorem PartOrdEmb.Limits.CoconePt.isCardinalFiltered_pt

Modification history

2026-05-28 18:39
Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean
feat(CategoryTheory): the category of κ-directed posets (#39669) …
Added PartOrdEmb.Limits.CoconePt.isCardinalFiltered_ptView on Github →