Commit 2026-03-20 20:15 7502683d

View on Github →

feat(Data/Sym/Sym2): fromRel & ToRel order isomorphism (#36467) This obsoletes the existing fromRel order embedding, but adds an order embedding for ToRel since it can avoid Subtype which makes it more useful (e.g. it shows ToRel is injective).

Estimated changes

Modified Mathlib/Data/Sym/Sym2.lean

added def Sym2.fromRelOrderIso

added theorem Sym2.fromRel_eq_fromRel_iff_eq

deleted theorem Sym2.fromRel_eq_fromRell_iff_eq

added def Sym2.toRelOrderEmbedding

added theorem Sym2.toRel_mono_iff