Def Mathlib.Meta.SetNotationForOrder.elabBinSetNotation

Modification history

2026-10-31 04:12

Mathlib/Tactic/SetNotationForOrder.lean

feat: use `max`/`min` for `union`/`inter` in `Set`, `Finset`, `ZFSet`, `Class` (#42316) …

Added Mathlib.Meta.SetNotationForOrder.elabBinSetNotation View on Github →