Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-19 04:59 7726a92f

View on Github →

feat(data/ordinal): sup, cofinality, subtraction

Estimated changes

Modified algebra/order.lean

added theorem le_of_forall_le

added theorem le_of_forall_lt

Modified algebra/ordered_ring.lean

added theorem zero_le_mul

Modified analysis/ennreal.lean

deleted theorem zero_le_mul

Modified analysis/metric_space.lean

Modified data/cardinal.lean

modified theorem cardinal.le_min

added theorem cardinal.le_one_iff_subsingleton

modified theorem cardinal.lift_min

modified def cardinal.min

modified theorem cardinal.min_eq

modified theorem cardinal.min_le

added theorem cardinal.nat_lt_omega

deleted theorem cardinal.nat_lt_ω

modified theorem cardinal.ne_zero_iff_nonempty

added def cardinal.omega

modified theorem cardinal.prop_eq_two

added theorem cardinal.succ_zero

added theorem cardinal.zero_lt_one

deleted def cardinal.ω

Modified data/fintype.lean

added theorem fintype.card_of_subtype

added theorem fintype.subtype_card

Modified data/ordinal.lean

added def cardinal.ord_eq_min

deleted theorem cardinal.ord_eq_min

added theorem cardinal.ord_nat

added theorem order_iso.cof.aux

added theorem order_iso.cof

added theorem ordinal.add_le_add_right

added theorem ordinal.add_lt_add_iff_left

added theorem ordinal.add_sub_cancel

added theorem ordinal.aleph'_succ

modified def ordinal.aleph

added def ordinal.bsup

added theorem ordinal.bsup_le

added theorem ordinal.card_eq_zero

added theorem ordinal.card_omega

added def ordinal.cof

added theorem ordinal.cof_eq_one_iff_is_succ

added theorem ordinal.cof_eq_zero

added theorem ordinal.cof_le_card

added theorem ordinal.cof_succ

added theorem ordinal.cof_type_le

added theorem ordinal.cof_zero

added theorem ordinal.exists_of_cof

added def ordinal.is_limit

modified theorem ordinal.le_add_left

added theorem ordinal.le_add_sub

added theorem ordinal.le_bsup

added theorem ordinal.le_cof_type

modified theorem ordinal.le_min

added theorem ordinal.le_sup

modified theorem ordinal.le_total

modified theorem ordinal.lift_min

added theorem ordinal.lift_omega

deleted theorem ordinal.lift_ω

added def ordinal.limit_rec_on

added theorem ordinal.lt_cof_type

added theorem ordinal.lt_of_add_lt_add_right

added theorem ordinal.lt_pred

added theorem ordinal.lt_sub

modified def ordinal.min

modified theorem ordinal.min_eq

modified theorem ordinal.min_le

added def ordinal.omega

added theorem ordinal.pos_of_is_limit

added def ordinal.pred

added theorem ordinal.pred_eq_iff_not_succ

added theorem ordinal.pred_le

added theorem ordinal.pred_le_self

added theorem ordinal.pred_lt_iff_is_succ

added theorem ordinal.pred_succ

added def ordinal.sub

added theorem ordinal.sub_le

added theorem ordinal.succ_inj

added theorem ordinal.succ_le

added theorem ordinal.succ_le_succ

added theorem ordinal.succ_lt_of_not_succ

added theorem ordinal.succ_lt_succ

added theorem ordinal.succ_nat_cast

added theorem ordinal.succ_ne_zero

added theorem ordinal.succ_pred_iff_is_succ

added theorem ordinal.succ_zero

added def ordinal.sup

added theorem ordinal.sup_le

added theorem ordinal.zero_or_succ_or_limit

deleted def ordinal.ω

Modified data/set/finite.lean

added theorem set.card_fintype_insert'

added theorem set.card_fintype_of_finset'

added theorem set.card_fintype_of_finset

added theorem set.card_insert

added theorem set.card_singleton

added theorem set.empty_card

Modified order/basic.lean

deleted theorem eq_of_le_of_forall_ge

added theorem eq_of_le_of_forall_ge_of_dense

deleted theorem eq_of_le_of_forall_le

added theorem eq_of_le_of_forall_le_of_dense

deleted theorem le_of_forall_ge

added theorem le_of_forall_ge_of_dense

deleted theorem le_of_forall_le

added theorem le_of_forall_le_of_dense