Commit 2026-07-27 19:23 9eb53bdd

View on Github →

chore: remove uses of Subrelation (#41450) Following up on the description of #40792, this removes additional uses of Subrelation now that #30526 has been merged.

Estimated changes

Modified Mathlib/Logic/Relation.lean

modified theorem Relation.EqvGen.eqvGen_le

modified theorem Relation.EqvGen.eqvGen_mono

modified theorem Relation.EqvGen.reflGen_le_eqvGen

modified theorem Relation.EqvGen.reflTransGen_le_eqvGen

modified theorem Relation.EqvGen.symmGen_le_eqvGen

modified theorem Relation.EqvGen.transGen_le_eqvGen

modified theorem Subrelation.antisymm

Modified Mathlib/Order/JordanHolder.lean