Commit 2023-02-16 08:59 b9f402c0

View on Github →

feat: port SetTheory.Ordinal.Arithmetic (#2271)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Ordinal/Arithmetic.lean

added theorem Acc.rank_eq

added theorem Acc.rank_lt_of_rel

added theorem Cardinal.add_one_of_aleph0_le

added theorem Cardinal.ord_aleph0

added theorem Ordinal.IsLimit.nat_lt

added theorem Ordinal.IsLimit.one_lt

added theorem Ordinal.IsLimit.pos

added theorem Ordinal.IsLimit.succ_lt

added def Ordinal.IsLimit

added theorem Ordinal.IsNormal.apply_omega

added theorem Ordinal.IsNormal.blsub_eq

added theorem Ordinal.IsNormal.bsup

added theorem Ordinal.IsNormal.bsup_eq

added theorem Ordinal.IsNormal.eq_iff_zero_and_succ

added theorem Ordinal.IsNormal.inj

added theorem Ordinal.IsNormal.isLimit

added theorem Ordinal.IsNormal.le_iff

added theorem Ordinal.IsNormal.le_iff_eq

added theorem Ordinal.IsNormal.le_set'

added theorem Ordinal.IsNormal.le_set

added theorem Ordinal.IsNormal.limit_le

added theorem Ordinal.IsNormal.limit_lt

added theorem Ordinal.IsNormal.lt_iff

added theorem Ordinal.IsNormal.monotone

added theorem Ordinal.IsNormal.refl

added theorem Ordinal.IsNormal.self_le

added theorem Ordinal.IsNormal.strictMono

added theorem Ordinal.IsNormal.sup

added theorem Ordinal.IsNormal.trans

added def Ordinal.IsNormal

added theorem Ordinal.add_eq_zero_iff

added theorem Ordinal.add_isLimit

added theorem Ordinal.add_isNormal

added theorem Ordinal.add_le_add_iff_right

added theorem Ordinal.add_le_of_forall_add_lt

added theorem Ordinal.add_le_of_limit

added theorem Ordinal.add_left_cancel

added theorem Ordinal.add_log_le_log_mul

added theorem Ordinal.add_mul_limit

added theorem Ordinal.add_mul_limit_aux

added theorem Ordinal.add_mul_succ

added theorem Ordinal.add_right_cancel

added theorem Ordinal.add_sub_add_cancel

added theorem Ordinal.add_sub_cancel

added theorem Ordinal.bddAbove_iff_small

added theorem Ordinal.bddAbove_of_small

added theorem Ordinal.bddAbove_range

added def Ordinal.bfamilyOfFamily'

added theorem Ordinal.bfamilyOfFamily'_typein

added def Ordinal.bfamilyOfFamily

added theorem Ordinal.bfamilyOfFamily_typein

added def Ordinal.blsub

added theorem Ordinal.blsub_comp

added theorem Ordinal.blsub_congr

added theorem Ordinal.blsub_const

added theorem Ordinal.blsub_eq_blsub

added theorem Ordinal.blsub_eq_lsub'

added theorem Ordinal.blsub_eq_lsub

added theorem Ordinal.blsub_eq_of_brange_eq

added theorem Ordinal.blsub_eq_zero_iff

added theorem Ordinal.blsub_id

added theorem Ordinal.blsub_le

added theorem Ordinal.blsub_le_bsup_succ

added theorem Ordinal.blsub_le_enumOrd

added theorem Ordinal.blsub_le_iff

added theorem Ordinal.blsub_le_of_brange_subset

added theorem Ordinal.blsub_one

added theorem Ordinal.blsub_pos

added theorem Ordinal.blsub_succ_of_mono

added theorem Ordinal.blsub_type

added theorem Ordinal.blsub_zero

added def Ordinal.bmex

added theorem Ordinal.bmex_le_blsub

added theorem Ordinal.bmex_le_of_ne

added theorem Ordinal.bmex_lt_ord_succ_card

added theorem Ordinal.bmex_monotone

added theorem Ordinal.bmex_not_mem_brange

added theorem Ordinal.bounded_singleton

added def Ordinal.brange

added theorem Ordinal.brange_bfamilyOfFamily'

added theorem Ordinal.brange_bfamilyOfFamily

added theorem Ordinal.brange_const

added def Ordinal.bsup

added theorem Ordinal.bsup_comp

added theorem Ordinal.bsup_congr

added theorem Ordinal.bsup_const

added theorem Ordinal.bsup_eq_blsub

added theorem Ordinal.bsup_eq_blsub_iff_lt_bsup

added theorem Ordinal.bsup_eq_blsub_iff_succ

added theorem Ordinal.bsup_eq_blsub_of_lt_succ_limit

added theorem Ordinal.bsup_eq_blsub_or_succ_bsup_eq_blsub

added theorem Ordinal.bsup_eq_bsup

added theorem Ordinal.bsup_eq_of_brange_eq

added theorem Ordinal.bsup_eq_sup'

added theorem Ordinal.bsup_eq_sup

added theorem Ordinal.bsup_eq_zero_iff

added theorem Ordinal.bsup_id_limit

added theorem Ordinal.bsup_id_succ

added theorem Ordinal.bsup_le

added theorem Ordinal.bsup_le_blsub

added theorem Ordinal.bsup_le_iff

added theorem Ordinal.bsup_le_of_brange_subset

added theorem Ordinal.bsup_not_succ_of_ne_bsup

added theorem Ordinal.bsup_one

added theorem Ordinal.bsup_succ_eq_blsub

added theorem Ordinal.bsup_succ_le_blsub

added theorem Ordinal.bsup_succ_of_mono

added theorem Ordinal.bsup_zero

added theorem Ordinal.card_mul

added theorem Ordinal.comp_bfamilyOfFamily'

added theorem Ordinal.comp_bfamilyOfFamily

added theorem Ordinal.comp_familyOfBFamily'

added theorem Ordinal.comp_familyOfBFamily

added theorem Ordinal.div_add_mod

added theorem Ordinal.div_def

added theorem Ordinal.div_eq_zero_of_lt

added theorem Ordinal.div_le

added theorem Ordinal.div_le_of_le_mul

added theorem Ordinal.div_lt

added theorem Ordinal.div_mul_cancel

added theorem Ordinal.div_nonempty

added theorem Ordinal.div_one

added theorem Ordinal.div_opow_log_lt

added theorem Ordinal.div_pos

added theorem Ordinal.div_self

added theorem Ordinal.div_zero

added theorem Ordinal.dvd_add_iff

added theorem Ordinal.dvd_antisymm

added theorem Ordinal.dvd_iff_mod_eq_zero

added theorem Ordinal.dvd_of_mod_eq_zero

added def Ordinal.enumOrd

added def Ordinal.enumOrdOrderIso

added theorem Ordinal.enumOrd_def'

added theorem Ordinal.enumOrd_def'_nonempty

added theorem Ordinal.enumOrd_def

added theorem Ordinal.enumOrd_def_nonempty

added theorem Ordinal.enumOrd_le_of_subset

added theorem Ordinal.enumOrd_mem

added theorem Ordinal.enumOrd_range

added theorem Ordinal.enumOrd_strictMono

added theorem Ordinal.enumOrd_succ_le

added theorem Ordinal.enumOrd_surjective

added theorem Ordinal.enumOrd_univ

added theorem Ordinal.enumOrd_zero

added theorem Ordinal.enum_succ_eq_top

added theorem Ordinal.eq_enumOrd

added theorem Ordinal.exists_of_lt_bmex

added theorem Ordinal.exists_of_lt_mex

added def Ordinal.familyOfBFamily'

added theorem Ordinal.familyOfBFamily'_enum

added def Ordinal.familyOfBFamily

added theorem Ordinal.familyOfBFamily_enum

added theorem Ordinal.has_succ_of_type_succ_lt

added theorem Ordinal.isLimit_add_iff

added theorem Ordinal.isLimit_iff_omega_dvd

added theorem Ordinal.isNormal_iff_lt_succ_and_blsub_eq

added theorem Ordinal.isNormal_iff_lt_succ_and_bsup_eq

added theorem Ordinal.isNormal_iff_strictMono_limit

added theorem Ordinal.le_add_sub

added theorem Ordinal.le_bmex_of_forall

added theorem Ordinal.le_bsup

added theorem Ordinal.le_div

added theorem Ordinal.le_mex_of_forall

added theorem Ordinal.le_mul_left

added theorem Ordinal.le_mul_right

added theorem Ordinal.le_of_dvd

added theorem Ordinal.le_of_mul_le_mul_left

added theorem Ordinal.le_sub_of_le

added theorem Ordinal.le_succ_of_isLimit

added theorem Ordinal.le_sup

added theorem Ordinal.le_sup_shrink_equiv

added theorem Ordinal.left_eq_zero_of_add_eq_zero

added theorem Ordinal.left_le_opow

added theorem Ordinal.lift_add

added theorem Ordinal.lift_isLimit

added theorem Ordinal.lift_is_succ

added theorem Ordinal.lift_mul

added theorem Ordinal.lift_nat_cast

added theorem Ordinal.lift_pred

added theorem Ordinal.lift_succ

added def Ordinal.limitRecOn

added theorem Ordinal.limitRecOn_limit

added theorem Ordinal.limitRecOn_succ

added theorem Ordinal.limitRecOn_zero

added theorem Ordinal.limit_le

added def Ordinal.log

added theorem Ordinal.log_def

added theorem Ordinal.log_eq_zero

added theorem Ordinal.log_le_self

added theorem Ordinal.log_mod_opow_log_lt_log_self

added theorem Ordinal.log_mono_right

added theorem Ordinal.log_nonempty

added theorem Ordinal.log_of_left_le_one

added theorem Ordinal.log_of_not_one_lt_left

added theorem Ordinal.log_one_left

added theorem Ordinal.log_one_right

added theorem Ordinal.log_opow

added theorem Ordinal.log_opow_mul_add

added theorem Ordinal.log_pos

added theorem Ordinal.log_zero_left

added theorem Ordinal.log_zero_right

added def Ordinal.lsub

added theorem Ordinal.lsub_const

added theorem Ordinal.lsub_empty

added theorem Ordinal.lsub_eq_blsub'

added theorem Ordinal.lsub_eq_blsub

added theorem Ordinal.lsub_eq_lsub

added theorem Ordinal.lsub_eq_of_range_eq

added theorem Ordinal.lsub_eq_zero_iff

added theorem Ordinal.lsub_le

added theorem Ordinal.lsub_le_iff

added theorem Ordinal.lsub_le_of_range_subset

added theorem Ordinal.lsub_le_sup_succ

added theorem Ordinal.lsub_not_mem_range

added theorem Ordinal.lsub_pos

added theorem Ordinal.lsub_sum

added theorem Ordinal.lsub_typein

added theorem Ordinal.lsub_unique

added theorem Ordinal.lt_add_of_limit

added theorem Ordinal.lt_blsub

added theorem Ordinal.lt_blsub_iff

added theorem Ordinal.lt_bsup

added theorem Ordinal.lt_bsup_of_limit

added theorem Ordinal.lt_bsup_of_ne_bsup

added theorem Ordinal.lt_div

added theorem Ordinal.lt_limit

added theorem Ordinal.lt_lsub

added theorem Ordinal.lt_lsub_iff

added theorem Ordinal.lt_mul_div_add

added theorem Ordinal.lt_mul_of_limit

added theorem Ordinal.lt_mul_succ_div

added theorem Ordinal.lt_omega

added theorem Ordinal.lt_opow_iff_log_lt

added theorem Ordinal.lt_opow_of_limit

added theorem Ordinal.lt_opow_succ_log_self

added theorem Ordinal.lt_pred

added theorem Ordinal.lt_sub

added theorem Ordinal.lt_sup

added theorem Ordinal.mem_brange

added theorem Ordinal.mem_brange_self

added def Ordinal.mex

added theorem Ordinal.mex_le_lsub

added theorem Ordinal.mex_le_of_ne

added theorem Ordinal.mex_lt_ord_succ_mk

added theorem Ordinal.mex_monotone

added theorem Ordinal.mex_not_mem_range

added theorem Ordinal.mk_initialSeg

added theorem Ordinal.mod_def

added theorem Ordinal.mod_eq_of_lt

added theorem Ordinal.mod_eq_zero_of_dvd

added theorem Ordinal.mod_lt

added theorem Ordinal.mod_one

added theorem Ordinal.mod_opow_log_lt_self

added theorem Ordinal.mod_self

added theorem Ordinal.mod_zero

added theorem Ordinal.mul_add_div

added theorem Ordinal.mul_div_cancel

added theorem Ordinal.mul_div_le

added theorem Ordinal.mul_isLimit

added theorem Ordinal.mul_isLimit_left

added theorem Ordinal.mul_isNormal

added theorem Ordinal.mul_le_mul_iff_left

added theorem Ordinal.mul_le_of_limit

added theorem Ordinal.mul_lt_mul_iff_left

added theorem Ordinal.mul_lt_mul_of_pos_left

added theorem Ordinal.mul_lt_of_lt_div

added theorem Ordinal.mul_ne_zero

added theorem Ordinal.mul_pos

added theorem Ordinal.mul_right_inj

added theorem Ordinal.mul_sub

added theorem Ordinal.mul_succ

added theorem Ordinal.nat_cast_div

added theorem Ordinal.nat_cast_eq_zero

added theorem Ordinal.nat_cast_inj

added theorem Ordinal.nat_cast_le

added theorem Ordinal.nat_cast_lt

added theorem Ordinal.nat_cast_mod

added theorem Ordinal.nat_cast_mul

added theorem Ordinal.nat_cast_ne_zero

added theorem Ordinal.nat_cast_opow

added theorem Ordinal.nat_cast_pos

added theorem Ordinal.nat_cast_sub

added theorem Ordinal.nat_lt_limit

added theorem Ordinal.nat_lt_omega

added theorem Ordinal.ne_bmex

added theorem Ordinal.ne_mex

added theorem Ordinal.ne_sup_iff_lt_sup

added theorem Ordinal.nonempty_compl_range

added theorem Ordinal.not_succ_isLimit

added theorem Ordinal.not_succ_of_isLimit

added theorem Ordinal.not_zero_isLimit

added theorem Ordinal.omega_isLimit

added theorem Ordinal.omega_le

added theorem Ordinal.omega_le_of_isLimit

added theorem Ordinal.omega_ne_zero

added theorem Ordinal.omega_pos

added theorem Ordinal.one_add_nat_cast

added theorem Ordinal.one_add_of_omega_le

added theorem Ordinal.one_add_omega

added theorem Ordinal.one_lt_omega

added theorem Ordinal.one_opow

added theorem Ordinal.opow_add

added theorem Ordinal.opow_def

added theorem Ordinal.opow_dvd_opow

added theorem Ordinal.opow_dvd_opow_iff

added theorem Ordinal.opow_isLimit

added theorem Ordinal.opow_isLimit_left

added theorem Ordinal.opow_isNormal

added theorem Ordinal.opow_le_iff_le_log

added theorem Ordinal.opow_le_of_limit

added theorem Ordinal.opow_le_opow_iff_right

added theorem Ordinal.opow_le_opow_left

added theorem Ordinal.opow_le_opow_right

added theorem Ordinal.opow_limit

added theorem Ordinal.opow_log_le_self

added theorem Ordinal.opow_lt_opow_iff_right

added theorem Ordinal.opow_lt_opow_left_of_succ

added theorem Ordinal.opow_mul

added theorem Ordinal.opow_mul_add_lt_opow_mul_succ

added theorem Ordinal.opow_mul_add_lt_opow_succ

added theorem Ordinal.opow_mul_add_pos

added theorem Ordinal.opow_ne_zero

added theorem Ordinal.opow_one

added theorem Ordinal.opow_one_add

added theorem Ordinal.opow_pos

added theorem Ordinal.opow_right_inj

added theorem Ordinal.opow_succ

added theorem Ordinal.opow_zero

added theorem Ordinal.out_no_max_of_succ_lt

added def Ordinal.pred

added theorem Ordinal.pred_eq_iff_not_succ'

added theorem Ordinal.pred_eq_iff_not_succ

added theorem Ordinal.pred_le

added theorem Ordinal.pred_le_self

added theorem Ordinal.pred_lt_iff_is_succ

added theorem Ordinal.pred_succ

added theorem Ordinal.pred_zero

added theorem Ordinal.range_enumOrd

added theorem Ordinal.range_familyOfBFamily'

added theorem Ordinal.range_familyOfBFamily

added theorem Ordinal.right_eq_zero_of_add_eq_zero

added theorem Ordinal.right_le_opow

added theorem Ordinal.smul_eq_mul

added theorem Ordinal.sub_eq_of_add_eq

added theorem Ordinal.sub_isLimit

added theorem Ordinal.sub_le

added theorem Ordinal.sub_le_self

added theorem Ordinal.sub_lt_of_le

added theorem Ordinal.sub_nonempty

added theorem Ordinal.sub_self

added theorem Ordinal.sub_sub

added theorem Ordinal.sub_zero

added theorem Ordinal.succ_log_def

added theorem Ordinal.succ_lt_of_isLimit

added theorem Ordinal.succ_lt_of_not_succ

added theorem Ordinal.succ_pred_iff_is_succ

added def Ordinal.sup

added theorem Ordinal.sup_add_nat

added theorem Ordinal.sup_const

added theorem Ordinal.sup_empty

added theorem Ordinal.sup_eq_bsup'

added theorem Ordinal.sup_eq_bsup

added theorem Ordinal.sup_eq_lsub

added theorem Ordinal.sup_eq_lsub_iff_lt_sup

added theorem Ordinal.sup_eq_lsub_iff_succ

added theorem Ordinal.sup_eq_lsub_or_sup_succ_eq_lsub

added theorem Ordinal.sup_eq_of_range_eq

added theorem Ordinal.sup_eq_sup

added theorem Ordinal.sup_eq_supₛ

added theorem Ordinal.sup_eq_zero_iff

added theorem Ordinal.sup_le

added theorem Ordinal.sup_le_iff

added theorem Ordinal.sup_le_lsub

added theorem Ordinal.sup_le_of_range_subset

added theorem Ordinal.sup_mul_nat

added theorem Ordinal.sup_nat_cast

added theorem Ordinal.sup_not_succ_of_ne_sup

added theorem Ordinal.sup_opow_nat

added theorem Ordinal.sup_succ_eq_lsub

added theorem Ordinal.sup_succ_le_lsub

added theorem Ordinal.sup_sum

added theorem Ordinal.sup_typein_limit

added theorem Ordinal.sup_typein_succ

added theorem Ordinal.sup_unique

added theorem Ordinal.supᵢ_ord

added theorem Ordinal.supₛ_eq_bsup

added theorem Ordinal.supₛ_eq_sup

added theorem Ordinal.supₛ_ord

added theorem Ordinal.type_prod_lex

added theorem Ordinal.type_subrel_lt

added theorem Ordinal.unbounded_range_of_sup_ge

added theorem Ordinal.zero_div

added theorem Ordinal.zero_mod

added theorem Ordinal.zero_opow'

added theorem Ordinal.zero_opow

added theorem Ordinal.zero_or_succ_or_limit

added theorem Ordinal.zero_sub

added theorem WellFounded.rank_eq

added theorem WellFounded.rank_lt_of_rel

added theorem WellFounded.rank_strictAnti

added theorem WellFounded.rank_strictMono

added theorem not_injective_of_ordinal

added theorem not_injective_of_ordinal_of_small

added theorem not_small_ordinal

added theorem not_surjective_of_ordinal

added theorem not_surjective_of_ordinal_of_small