Commit 2025-01-26 13:15 bc0287e5

View on Github →

feat(Order/Antisymmetrization): AntisymmRel lemmas (#19571) These are mostly ported from SetTheory.PGame.Equiv.

Estimated changes

Modified Mathlib/Order/Antisymmetrization.lean

added theorem AntisymmRel.antisymmRel_congr

added theorem AntisymmRel.antisymmRel_congr_left

added theorem AntisymmRel.antisymmRel_congr_right

added theorem AntisymmRel.ge

modified theorem AntisymmRel.image

added theorem AntisymmRel.le

added theorem AntisymmRel.le_congr

added theorem AntisymmRel.le_congr_left

added theorem AntisymmRel.le_congr_right

added theorem AntisymmRel.lt_congr

added theorem AntisymmRel.lt_congr_left

added theorem AntisymmRel.lt_congr_right

added theorem AntisymmRel.rfl

modified theorem AntisymmRel.symm

modified theorem AntisymmRel.trans

added theorem antisymmRel_comm

modified theorem antisymmRel_iff_eq

added theorem le_iff_lt_or_antisymmRel

added theorem le_of_antisymmRel_of_le

added theorem le_of_le_of_antisymmRel

added theorem lt_of_antisymmRel_of_lt

added theorem lt_of_lt_of_antisymmRel

Modified Mathlib/Order/RelClasses.lean

added theorem rel_congr

added theorem rel_congr_left

added theorem rel_congr_right