Theorem Sym2.inf_eq_inf_and_sup_eq_sup

Modification history

2025-04-14 15:20
Mathlib/Data/Sym/Sym2/Order.lean
feat(Sym2/Order): `s.inf = t.inf ∧ s.sup = t.sup ↔ s = t` (#24005) …
Added Sym2.inf_eq_inf_and_sup_eq_supView on Github →