Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-04-07 22:13 f29120f8

View on Github →

chore(order/rel_iso/basic): better namespace management (#18758) We remove a lot of _root_ by simply closing and reopening a namespace.

Estimated changes

modified theorem acc_lift_on₂'_iff
modified theorem acc_lift₂_iff
modified def quotient.mk_rel_hom
modified theorem well_founded_lift₂_iff