Commit 2025-04-14 15:20 22da9880

feat(Sym2/Order): s.inf = t.inf ∧ s.sup = t.sup ↔ s = t (#24005) Characterize equality of two symmetric squares. In a linear order, two symmetric squares are equal if and only if they have the same infimum and supremum.