Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2017-12-21 06:51
5f4d8909
View on Github →
feat(data/ordinal): omega is least limit ordinal
Estimated changes
Modified
algebra/order.lean
modified
theorem
le_iff_le_iff_lt_iff_lt
modified
theorem
le_imp_le_iff_lt_imp_lt
Modified
data/cardinal.lean
added
theorem
cardinal.le_lift_iff
added
theorem
cardinal.lift_omega
added
theorem
cardinal.lt_lift_iff
added
theorem
cardinal.lt_omega_iff_finite
added
theorem
cardinal.lt_omega_iff_fintype
Modified
data/ordinal.lean
modified
theorem
cardinal.card_ord
added
theorem
cardinal.lift_ord
modified
theorem
cardinal.ord_le_ord
modified
theorem
cardinal.ord_lt_ord
modified
theorem
cardinal.ord_nat
added
theorem
cardinal.ord_omega
added
theorem
ordinal.card_eq_nat
added
theorem
ordinal.card_le_nat
added
theorem
ordinal.card_lt_nat
added
theorem
ordinal.fintype_card
added
theorem
ordinal.le_lift_iff
added
theorem
ordinal.lift_down'
modified
theorem
ordinal.lift_down
added
theorem
ordinal.lift_nat_cast
added
theorem
ordinal.lift_type_fin
added
theorem
ordinal.lt_lift_iff
added
theorem
ordinal.lt_omega
added
theorem
ordinal.nat_cast_inj
added
theorem
ordinal.nat_cast_le
added
theorem
ordinal.nat_cast_lt
added
theorem
ordinal.nat_le_card
added
theorem
ordinal.nat_lt_card
added
theorem
ordinal.nat_lt_limit
added
theorem
ordinal.nat_lt_omega
added
theorem
ordinal.omega_is_limit
added
theorem
ordinal.omega_le
added
theorem
ordinal.omega_le_of_is_limit
added
theorem
ordinal.type_fin
Modified
logic/basic.lean
added
theorem
false_ne_true
deleted
theorem
false_neq_true
modified
theorem
iff_of_eq
Modified
logic/schroeder_bernstein.lean
modified
theorem
function.embedding.injective_min
Modified
order/order_iso.lean
added
def
fin.val.order_embedding
added
def
fin_fin.order_embedding
added
def
order_iso.to_order_embedding