Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-17 02:45 b19c222c

View on Github →

feat(data/ordinal): ordinal collapse, ordinals ordering,

Estimated changes

Modified algebra/group_power.lean

Modified data/cardinal.lean

added theorem cardinal.embedding.sum_congr_apply_inl

added theorem cardinal.embedding.sum_congr_apply_inr

added def cardinal.mk

Modified data/equiv.lean

added def equiv.empty_prod

added def equiv.empty_sum

added theorem equiv.prod_congr_apply

added def equiv.prod_empty

deleted def equiv.prod_empty_left

deleted def equiv.prod_empty_right

added def equiv.prod_unit

deleted def equiv.prod_unit_left

deleted def equiv.prod_unit_right

added theorem equiv.sum_assoc_apply_in1

added theorem equiv.sum_assoc_apply_in2

added theorem equiv.sum_assoc_apply_in3

added theorem equiv.sum_congr_apply_inl

added theorem equiv.sum_congr_apply_inr

added def equiv.sum_empty

deleted def equiv.sum_empty_left

deleted def equiv.sum_empty_right

added def equiv.unit_prod

Modified data/ordinal.lean

added def cardinal.ord

added theorem cardinal.ord_eq

added theorem cardinal.ord_eq_min

added theorem cardinal.ord_le

added theorem cardinal.ord_le_ord

added def initial_seg.le_add

added theorem initial_seg.le_add_apply

added def order_embedding.collapse

added theorem order_embedding.collapse_F.lt

added theorem order_embedding.collapse_F.not_lt

added def order_embedding.collapse_F

added theorem order_embedding.collapse_apply

added def order_embedding.of_monotone

deleted theorem order_embedding.of_monotone

added theorem order_embedding.of_monotone_coe

added def order_embedding.preimage

added theorem ordinal.add_le_add_iff_left

added theorem ordinal.add_le_add_left

added theorem ordinal.add_succ

added theorem ordinal.card_add

added theorem ordinal.card_le_card

added theorem ordinal.card_one

added theorem ordinal.card_zero

added theorem ordinal.le_add_left

added theorem ordinal.le_add_right

added theorem ordinal.le_min

added theorem ordinal.le_total

added def ordinal.min

added theorem ordinal.min_eq

added theorem ordinal.min_le

added def ordinal.succ

added theorem ordinal.type_le_of_order_embedding

added theorem ordinal.zero_le

deleted def prod.lex.is_well_order

deleted def sum.lex.is_well_order

added theorem well_founded.has_min

added def well_founded.min

added theorem well_founded.min_mem

added theorem well_founded.not_lt_min

Modified data/set/basic.lean

modified theorem set.mem_range

added theorem set.mem_range_self

Modified logic/basic.lean

added def empty.elim

deleted theorem empty.elim

Modified order/complete_lattice.lean

Modified tactic/alias.lean

Modified tactic/interactive.lean