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