Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-11 23:10 58d97787

View on Github →

chore(set_theory/ordinal/arithmetic): clean up is_normal.sup and related (#15162) We golf various theorems and tweak their arguments.

Estimated changes

modified theorem ordinal.is_normal.is_limit
modified theorem ordinal.is_normal.le_iff_eq
modified theorem ordinal.is_normal.le_set'
modified theorem ordinal.is_normal.le_set
modified theorem ordinal.is_normal.refl
modified theorem ordinal.is_normal.sup
modified theorem ordinal.is_normal.trans