Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-18 08:38 f6bbca71

View on Github →

feat(data/ordinal): universe lifts, alephs

Estimated changes

Modified algebra/big_operators.lean

added theorem finset.card_sigma

Modified algebra/group_power.lean

added theorem nat.smul_eq_mul

Modified algebra/module.lean

Modified data/cardinal.lean

added theorem cardinal.add_one_le_succ

added theorem cardinal.fintype_card

added theorem cardinal.le_mk_iff_exists_set

added def cardinal.lift

added theorem cardinal.lift_add

added theorem cardinal.lift_id

added theorem cardinal.lift_inj

added theorem cardinal.lift_le

added theorem cardinal.lift_lift

added theorem cardinal.lift_lt

added theorem cardinal.lift_min

added theorem cardinal.lift_mk

added theorem cardinal.lift_mk_eq

added theorem cardinal.lift_mk_fin

added theorem cardinal.lift_mk_le

added theorem cardinal.lift_mul

added theorem cardinal.lift_nat_cast

added theorem cardinal.lift_one

added theorem cardinal.lift_power

added theorem cardinal.lift_umax

added theorem cardinal.lift_zero

added theorem cardinal.lt_succ_self

added theorem cardinal.mk_def

added theorem cardinal.mk_fin

added theorem cardinal.nat_cast_inj

added theorem cardinal.nat_cast_le

added theorem cardinal.nat_cast_lt

added theorem cardinal.nat_lt_ω

added theorem cardinal.nat_succ

added def cardinal.succ

added theorem cardinal.succ_le

modified def cardinal.ω

Modified data/finset.lean

modified theorem finset.bind_mono

added theorem finset.card_image_of_inj_on

added theorem finset.card_image_of_injective

added theorem finset.card_product

Modified data/fintype.lean

added theorem finset.eq_univ_iff_forall

modified theorem finset.mem_univ

modified theorem finset.mem_univ_val

added theorem fintype.card_bool

added theorem fintype.card_congr

added theorem fintype.card_empty

added theorem fintype.card_eq

added theorem fintype.card_fin

added theorem fintype.card_prod

added theorem fintype.card_sigma

added theorem fintype.card_sum

added theorem fintype.card_ulift

added theorem fintype.card_unit

modified def fintype.of_equiv

added theorem fintype.of_equiv_card

added theorem fintype.univ_bool

added theorem fintype.univ_empty

added theorem fintype.univ_unit

Modified data/list/basic.lean

added theorem list.length_pmap

added theorem list.nth_le_index_of

Modified data/multiset.lean

added theorem multiset.card_bind

added theorem multiset.card_join

added theorem multiset.card_map

added theorem multiset.card_pmap

added theorem multiset.card_product

added theorem multiset.card_sigma

Modified data/ordinal.lean

added theorem cardinal.aleph_idx.init

added def cardinal.aleph_idx.initial_seg

added theorem cardinal.aleph_idx.initial_seg_coe

added def cardinal.aleph_idx.order_iso

added theorem cardinal.aleph_idx.order_iso_coe

added def cardinal.aleph_idx

added theorem cardinal.aleph_idx_le

added theorem cardinal.aleph_idx_lt

added theorem cardinal.card_ord

added theorem cardinal.lt_ord

added def cardinal.ord.order_embedding

added theorem cardinal.ord.order_embedding_coe

modified theorem cardinal.ord_eq_min

modified theorem cardinal.ord_le

modified theorem cardinal.ord_le_ord

added theorem cardinal.ord_le_type

added theorem cardinal.ord_lt_ord

added theorem cardinal.ord_zero

added def order.cof

deleted theorem order_iso.of_surjective_apply

added theorem order_iso.of_surjective_coe

added theorem order_iso.prod_lex_congr

added theorem order_iso.sum_lex_congr

added def ordinal.aleph'.order_iso

added theorem ordinal.aleph'.order_iso_coe

added def ordinal.aleph'

added theorem ordinal.aleph'_aleph_idx

added theorem ordinal.aleph'_le

added theorem ordinal.aleph'_lt

added def ordinal.aleph

added theorem ordinal.aleph_idx_aleph'

added theorem ordinal.card_nat

added theorem ordinal.card_type

added def ordinal.lift.initial_seg

added theorem ordinal.lift.initial_seg_coe

added def ordinal.lift.principal_seg

added theorem ordinal.lift.principal_seg_coe

added theorem ordinal.lift.principal_seg_top'

added theorem ordinal.lift.principal_seg_top

added def ordinal.lift

added theorem ordinal.lift_add

added theorem ordinal.lift_down

added theorem ordinal.lift_id

added theorem ordinal.lift_inj

added theorem ordinal.lift_le

added theorem ordinal.lift_lift

added theorem ordinal.lift_lt

added theorem ordinal.lift_min

added theorem ordinal.lift_mul

added theorem ordinal.lift_one

added theorem ordinal.lift_type_eq

added theorem ordinal.lift_type_le

added theorem ordinal.lift_type_lt

added theorem ordinal.lift_umax

added theorem ordinal.lift_zero

added theorem ordinal.lift_ω

added theorem ordinal.lt_succ_self

added theorem ordinal.ord_card_le

added theorem ordinal.type_le'

deleted theorem ordinal.type_le_of_order_embedding

added def ordinal.typein.principal_seg

added theorem ordinal.typein.principal_seg_coe

added def ordinal.ω