Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-06 19:03 e18972b3

View on Github →

feat(set_theory/ordinal_arithmetic): Suprema of empty families (#11872)

Estimated changes

deleted theorem ordinal.blsub_eq_zero
added theorem ordinal.blsub_zero
added theorem ordinal.bsup_zero
added theorem ordinal.lsub_empty
deleted theorem ordinal.lsub_eq_zero
added theorem ordinal.sup_empty