Mathlib Changelog
v3
Changelog
About
Github
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