Def Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.φ

Modification history

2026-07-24 07:15
Mathlib/CategoryTheory/Presentable/SharplyLT/Basic.lean
chore: add missing `noncomputable` (#41446) …
Deleted Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.φView on Github →
2026-07-03 08:36
Mathlib/CategoryTheory/Presentable/SharplyLT/Basic.lean
feat(CategoryTheory/Presentable): sharply smaller regular cardinals (#40937) …
Added Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.φView on Github →