Def iInf_delab

Modification history

2025-11-19 06:07
Mathlib/Order/SetNotation.lean
chore: move Mathlib to the module system (#31786) …
Deleted iInf_delabView on Github →
2024-04-09 03:53
Mathlib/Order/SetNotation.lean
fix: add missing withOverApps (#12022) …
Modified iInf_delabView on Github →
2024-02-11 19:22
Mathlib/Order/CompleteLattice.lean
chore(Order/*): move `SupSet`, `Set.sUnion` etc to a new file (#10232)
Modified iInf_delabView on Github →
2023-10-13 21:18
Mathlib/Order/CompleteLattice.lean
feat: long overdue delaborators (#7633) …
Added iInf_delabView on Github →