Theorem ciInf_eq_top_of_top_mem

Modification history

2026-04-05 00:51
Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
chore(Order/ConditionallyCompleteLattice/Indexed): fix typo in theorem name (#37650) …
Deleted ciInf_eq_top_of_top_memView on Github →
2024-10-22 14:55
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
refactor(Order/ConditionallyCompleteLattice): split large file (#18029)
Modified ciInf_eq_top_of_top_memView on Github →
2024-10-16 12:56
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
feat(SetTheory/Ordinal/Enum): more lemmas on `enumOrd` (#17668)
Added ciInf_eq_top_of_top_memView on Github →