Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-10 08:36 a758ffb3

View on Github →

feat(data/ordinal): ordinal numbers

Estimated changes

Modified data/cardinal.lean

modified theorem cardinal.add_mono

modified theorem cardinal.le_iff_exists_add

modified theorem cardinal.mul_mono

modified theorem cardinal.mul_power

modified theorem cardinal.one_power

modified theorem cardinal.power_mono_left

modified theorem cardinal.power_mono_right

modified theorem cardinal.power_mul

modified theorem cardinal.power_sum

modified theorem cardinal.power_zero

modified theorem cardinal.prop_eq_two

modified theorem cardinal.zero_le

modified theorem cardinal.zero_power

modified theorem embedding.antisymm

added theorem embedding.inj'

added theorem embedding.refl_apply

modified theorem embedding.schroeder_bernstein

added theorem embedding.to_fun_eq_coe

modified theorem embedding.total

added theorem embedding.trans_apply

deleted theorem equiv.of_bijective

added theorem equiv.to_embedding_coe_fn

Modified data/equiv.lean

added theorem equiv.cast_apply

deleted theorem equiv.comp_apply

deleted def equiv.id

deleted theorem equiv.id_apply

added theorem equiv.of_bijective_to_fun

added theorem equiv.refl_apply

added theorem equiv.set.image_apply

added theorem equiv.set.range_apply

modified theorem equiv.swap_self

modified theorem equiv.swap_swap

added theorem equiv.trans_apply

Modified data/nat/basic.lean

added def nat.foldl

added def nat.foldr

Created data/ordinal.lean

added structure Well_order

added theorem initial_seg.antisymm.aux

added def initial_seg.antisymm

added theorem initial_seg.antisymm_symm

added theorem initial_seg.antisymm_to_fun

added theorem initial_seg.coe_fn_mk

added theorem initial_seg.coe_fn_to_order_embedding

added theorem initial_seg.eq_or_principal

added theorem initial_seg.init'

added theorem initial_seg.init_iff

added def initial_seg.of_iso

added theorem initial_seg.of_iso_apply

added theorem initial_seg.refl_apply

added theorem initial_seg.trans_apply

added def initial_seg.unique_of_extensional

added structure initial_seg

added def is_irrefl.swap

added def is_irrefl_of_is_asymm

added def is_strict_order.swap

added def is_strict_total_order'.swap

added def is_strict_weak_order_of_is_order_connected

added def is_trans.swap

added def is_trichotomous.swap

added def order.preimage

added theorem order_embedding.coe_fn_mk

added theorem order_embedding.coe_fn_to_embedding

added theorem order_embedding.eq_of_to_fun_eq

added theorem order_embedding.eq_preimage

added theorem order_embedding.nat_lt

added theorem order_embedding.of_monotone

added theorem order_embedding.ord'

added theorem order_embedding.refl_apply

added def order_embedding.rsymm

added theorem order_embedding.trans_apply

added theorem order_embedding.well_founded_iff_no_descending_seq

added structure order_embedding

added theorem order_iso.apply_inverse_apply

added theorem order_iso.coe_coe_fn

added theorem order_iso.coe_fn_mk

added theorem order_iso.coe_fn_symm_mk

added theorem order_iso.coe_fn_to_equiv

added theorem order_iso.eq_of_to_fun_eq

added theorem order_iso.inverse_apply_apply

added def order_iso.of_surjective

added theorem order_iso.of_surjective_apply

added theorem order_iso.ord'

added def order_iso.preimage

added theorem order_iso.refl_apply

added theorem order_iso.trans_apply

added structure order_iso

added def ordinal.card

added def ordinal.le

added def ordinal.lt

added def ordinal

added theorem principal_seg.coe_coe_fn'

added theorem principal_seg.coe_coe_fn

added theorem principal_seg.coe_fn_mk

added theorem principal_seg.coe_fn_to_order_embedding

added theorem principal_seg.down'

added def principal_seg.equiv_lt

added theorem principal_seg.equiv_lt_apply

added theorem principal_seg.init

added theorem principal_seg.init_iff

added theorem principal_seg.irrefl

added def principal_seg.le_lt

added theorem principal_seg.le_lt_apply

added def principal_seg.lt_le

added theorem principal_seg.lt_le_apply

added theorem principal_seg.trans_apply

added structure principal_seg

added def set_coe_embedding

Modified data/set/basic.lean

added theorem set.set_coe_cast