Def iInf_delab

Modification history

2024-04-09 03:53

Mathlib/Order/SetNotation.lean

fix: add missing withOverApps (#12022) …

Modified iInf_delab View 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_delab View on Github →

2023-10-13 21:18

Mathlib/Order/CompleteLattice.lean

feat: long overdue delaborators (#7633) …

Added iInf_delab View on Github →