Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-05 20:50 769a9349

View on Github →

feat(set_theory/*) cardinal.min → Inf (#13410) We discard cardinal.min in favor of Inf (the original definition is really just infi). Note: lift_min' is renamed to lift_min, as the name clash no longer exists. For consistency, lift_max' is renamed to lift_max and lift_max is renamed to lift_umax_eq.

Estimated changes

added theorem cardinal.Inf_empty
deleted theorem cardinal.le_min
added theorem cardinal.lift_Inf
deleted theorem cardinal.lift_max'
modified theorem cardinal.lift_max
deleted theorem cardinal.lift_min'
modified theorem cardinal.lift_min
added theorem cardinal.lift_monotone
added theorem cardinal.lift_umax_eq
deleted theorem cardinal.min_eq
deleted theorem cardinal.min_le
modified theorem cardinal.sup_eq_zero
modified def order.cof
modified theorem order.cof_le
added theorem order.cof_nonempty
modified theorem ordinal.lift_cof
deleted theorem rel_iso.cof.aux
deleted theorem rel_iso.cof
added theorem rel_iso.cof_eq
added theorem rel_iso.cof_eq_lift
added theorem rel_iso.cof_le
added theorem rel_iso.cof_le_lift
modified def strict_order.cof
modified theorem function.embedding.total