Def Mathlib.Meta.SetNotationForOrder.elabSubsetLike

Modification history

2026-10-31 04:12

Mathlib/Tactic/SetNotationForOrder.lean

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

Deleted Mathlib.Meta.SetNotationForOrder.elabSubsetLike View on Github →

2026-05-12 10:45

Mathlib/Tactic/SetNotationForOrder.lean

feat: implementation of `@[use_set_notation_for_order]` (#37347) …

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