Commit 2026-07-06 13:36 cef1e7de

View on Github →

feat: lemmas about equality of EqvGen (#40792) I've named the lemmas about Subrelation with _le_, so that if/when #30526 lands, the names can be kept.

Estimated changes

Modified Mathlib/Logic/Relation.lean

added theorem Relation.EqvGen.eqvGen_eq_reflTransGen

added theorem Relation.EqvGen.eqvGen_le

added theorem Relation.EqvGen.eqvGen_mono

added theorem Relation.EqvGen.eqvGen_reflGen

added theorem Relation.EqvGen.eqvGen_reflTransGen

added theorem Relation.EqvGen.eqvGen_symmGen

added theorem Relation.EqvGen.eqvGen_transGen

added theorem Relation.EqvGen.reflGen_le_eqvGen

added theorem Relation.EqvGen.reflTransGen_le_eqvGen

added theorem Relation.EqvGen.reflTransGen_symmGen

added theorem Relation.EqvGen.symmGen_le_eqvGen

added theorem Relation.EqvGen.transGen_le_eqvGen

modified theorem Relation.equivalence_join

added theorem Subrelation.antisymm