Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-18 18:32 fdd7e98c

View on Github →

feat(set_theory/*): Redefine sup f as supr f (#12657)

Estimated changes

Modified src/data/W/cardinal.lean

Modified src/linear_algebra/dimension.lean

Modified src/measure_theory/card_measurable_space.lean

Modified src/set_theory/cardinal.lean

added theorem cardinal.bdd_above_range

deleted theorem cardinal.nonempty_sup

modified theorem cardinal.sup_le

added theorem cardinal.sup_le_iff

Modified src/set_theory/cofinality.lean

Modified src/set_theory/ordinal_arithmetic.lean

added theorem ordinal.Sup_eq_bsup

added theorem ordinal.Sup_eq_sup

added theorem ordinal.bdd_above_range

modified theorem ordinal.blsub_le

added theorem ordinal.blsub_le_iff

modified theorem ordinal.bsup_le

added theorem ordinal.bsup_le_iff

modified theorem ordinal.lsub_le

added theorem ordinal.lsub_le_iff

deleted theorem ordinal.lt_sup_of_ne_sup

added theorem ordinal.ne_sup_iff_lt_sup

modified theorem ordinal.nfp_le

added theorem ordinal.nfp_le_iff

modified theorem ordinal.sup_le

added theorem ordinal.sup_le_iff

deleted theorem ordinal.sup_nonempty

Modified src/set_theory/ordinal_topology.lean

Modified src/set_theory/principal.lean