Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-08 19:01 acf8294d

View on Github →

feat(order/rel_iso): well_founded (quotient.lift₂ r H) ↔ well_founded r (#15890)

Estimated changes

Modified src/logic/embedding.lean

added theorem function.embedding.coe_quotient_out

Modified src/order/rel_iso.lean

added theorem well_founded_lift₂_iff