Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-23 15:25 3353f661

View on Github →

chore(*): golf using acc_lift₂_iff and well_founded_lift₂_iff (#18526)

Estimated changes

Modified src/order/antisymmetrization.lean

Modified src/order/rel_iso/basic.lean

added theorem acc_lift_on₂'_iff

added theorem acc_lift₂_iff

added def quotient.mk_rel_hom

added theorem well_founded_lift_on₂'_iff

modified theorem well_founded_lift₂_iff

Modified src/set_theory/zfc/basic.lean

modified theorem Set.mem_wf