Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-23 11:08 b9beca0b

View on Github →

chore(set_theory/ordinal): split into multiple files (#3517) Split the file ordinal.lean into three files, and add docstrings for all definitions and file-level docstrings. This is just shuffling things around: no new content, no erased content.

Estimated changes

added theorem cardinal.add_eq_left
added theorem cardinal.add_eq_max
added theorem cardinal.add_eq_right
added theorem cardinal.add_eq_self
added theorem cardinal.add_lt_of_lt
added theorem cardinal.add_one_eq
added def cardinal.aleph'
added theorem cardinal.aleph'_le
added theorem cardinal.aleph'_lt
added theorem cardinal.aleph'_nat
added theorem cardinal.aleph'_omega
added theorem cardinal.aleph'_succ
added theorem cardinal.aleph'_zero
added def cardinal.aleph
added theorem cardinal.aleph_idx_le
added theorem cardinal.aleph_idx_lt
added theorem cardinal.aleph_le
added theorem cardinal.aleph_lt
added theorem cardinal.aleph_succ
added theorem cardinal.aleph_zero
added theorem cardinal.bit0_eq_self
added theorem cardinal.bit0_le_bit0
added theorem cardinal.bit0_le_bit1
added theorem cardinal.bit0_lt_bit0
added theorem cardinal.bit0_lt_bit1
added theorem cardinal.bit0_lt_omega
added theorem cardinal.bit0_ne_zero
added theorem cardinal.bit1_le_bit0
added theorem cardinal.bit1_le_bit1
added theorem cardinal.bit1_lt_bit0
added theorem cardinal.bit1_lt_bit1
added theorem cardinal.bit1_lt_omega
added theorem cardinal.bit1_ne_zero
added theorem cardinal.exists_aleph
added theorem cardinal.le_mul_left
added theorem cardinal.le_mul_right
added theorem cardinal.mk_cardinal
added theorem cardinal.mk_list_eq_mk
added theorem cardinal.mul_eq_left
added theorem cardinal.mul_eq_max
added theorem cardinal.mul_eq_right
added theorem cardinal.mul_eq_self
added theorem cardinal.mul_lt_of_lt
added theorem cardinal.omega_le_bit0
added theorem cardinal.omega_le_bit1
added theorem cardinal.one_le_bit0
added theorem cardinal.one_le_bit1
added theorem cardinal.one_le_one
added theorem cardinal.one_lt_bit0
added theorem cardinal.one_lt_bit1
added theorem cardinal.one_lt_two
added theorem cardinal.ord_is_limit
added theorem cardinal.pow_le
added theorem cardinal.power_nat_le
added theorem cardinal.power_self_eq
added theorem cardinal.powerlt_omega
added theorem cardinal.type_cardinal
added theorem cardinal.zero_lt_bit0
added theorem cardinal.zero_lt_bit1
deleted theorem cardinal.add_eq_left
deleted theorem cardinal.add_eq_left_iff
deleted theorem cardinal.add_eq_max
deleted theorem cardinal.add_eq_right
deleted theorem cardinal.add_eq_right_iff
deleted theorem cardinal.add_eq_self
deleted theorem cardinal.add_lt_of_lt
deleted theorem cardinal.add_one_eq
deleted def cardinal.aleph'
deleted theorem cardinal.aleph'_aleph_idx
deleted theorem cardinal.aleph'_is_normal
deleted theorem cardinal.aleph'_le
deleted theorem cardinal.aleph'_lt
deleted theorem cardinal.aleph'_nat
deleted theorem cardinal.aleph'_omega
deleted theorem cardinal.aleph'_succ
deleted theorem cardinal.aleph'_zero
deleted def cardinal.aleph
deleted theorem cardinal.aleph_idx.init
deleted def cardinal.aleph_idx
deleted theorem cardinal.aleph_idx_aleph'
deleted theorem cardinal.aleph_idx_le
deleted theorem cardinal.aleph_idx_lt
deleted theorem cardinal.aleph_is_normal
deleted theorem cardinal.aleph_le
deleted theorem cardinal.aleph_lt
deleted theorem cardinal.aleph_succ
deleted theorem cardinal.aleph_zero
deleted theorem cardinal.bit0_eq_self
deleted theorem cardinal.bit0_le_bit0
deleted theorem cardinal.bit0_le_bit1
deleted theorem cardinal.bit0_lt_bit0
deleted theorem cardinal.bit0_lt_bit1
deleted theorem cardinal.bit0_lt_omega
deleted theorem cardinal.bit0_ne_zero
deleted theorem cardinal.bit1_eq_self_iff
deleted theorem cardinal.bit1_le_bit0
deleted theorem cardinal.bit1_le_bit1
deleted theorem cardinal.bit1_lt_bit0
deleted theorem cardinal.bit1_lt_bit1
deleted theorem cardinal.bit1_lt_omega
deleted theorem cardinal.bit1_ne_zero
deleted theorem cardinal.exists_aleph
deleted theorem cardinal.extend_function
deleted theorem cardinal.le_mul_left
deleted theorem cardinal.le_mul_right
deleted theorem cardinal.mk_cardinal
deleted theorem cardinal.mk_list_eq_mk
deleted theorem cardinal.mul_eq_left
deleted theorem cardinal.mul_eq_left_iff
deleted theorem cardinal.mul_eq_max
deleted theorem cardinal.mul_eq_right
deleted theorem cardinal.mul_eq_self
deleted theorem cardinal.mul_lt_of_lt
deleted theorem cardinal.omega_le_aleph'
deleted theorem cardinal.omega_le_aleph
deleted theorem cardinal.omega_le_bit0
deleted theorem cardinal.omega_le_bit1
deleted theorem cardinal.one_le_bit0
deleted theorem cardinal.one_le_bit1
deleted theorem cardinal.one_le_one
deleted theorem cardinal.one_lt_bit0
deleted theorem cardinal.one_lt_bit1
deleted theorem cardinal.one_lt_two
deleted theorem cardinal.ord_is_limit
deleted theorem cardinal.ord_omega
deleted theorem cardinal.pow_le
deleted theorem cardinal.power_nat_le
deleted theorem cardinal.power_self_eq
deleted theorem cardinal.powerlt_omega
deleted theorem cardinal.powerlt_omega_le
deleted theorem cardinal.type_cardinal
deleted theorem cardinal.zero_lt_bit0
deleted theorem cardinal.zero_lt_bit1
deleted def ordinal.CNF
deleted theorem ordinal.CNF_aux
deleted theorem ordinal.CNF_foldr
deleted theorem ordinal.CNF_fst_le
deleted theorem ordinal.CNF_fst_le_log
deleted theorem ordinal.CNF_ne_zero
deleted theorem ordinal.CNF_pairwise
deleted theorem ordinal.CNF_pairwise_aux
deleted theorem ordinal.CNF_rec_ne_zero
deleted theorem ordinal.CNF_rec_zero
deleted theorem ordinal.CNF_snd_lt
deleted theorem ordinal.CNF_sorted
deleted theorem ordinal.CNF_zero
deleted theorem ordinal.add_absorp
deleted theorem ordinal.add_absorp_iff
deleted theorem ordinal.add_is_limit
deleted theorem ordinal.add_is_normal
deleted theorem ordinal.add_le_of_limit
deleted theorem ordinal.add_left_cancel
deleted theorem ordinal.add_lt_omega
deleted theorem ordinal.add_mul_limit
deleted theorem ordinal.add_mul_limit_aux
deleted theorem ordinal.add_mul_succ
deleted theorem ordinal.add_omega
deleted theorem ordinal.add_omega_power
deleted theorem ordinal.add_right_cancel
deleted theorem ordinal.add_sub_cancel
deleted theorem ordinal.add_succ
deleted def ordinal.bsup
deleted theorem ordinal.bsup_id
deleted theorem ordinal.bsup_le
deleted theorem ordinal.bsup_type
deleted theorem ordinal.card_eq_nat
deleted theorem ordinal.card_eq_zero
deleted theorem ordinal.card_le_nat
deleted theorem ordinal.card_lt_nat
deleted theorem ordinal.card_mul
deleted theorem ordinal.card_succ
deleted def ordinal.deriv
deleted theorem ordinal.deriv_is_normal
deleted theorem ordinal.deriv_limit
deleted theorem ordinal.deriv_succ
deleted theorem ordinal.deriv_zero
deleted theorem ordinal.div_add_mod
deleted theorem ordinal.div_def
deleted theorem ordinal.div_eq_zero_of_lt
deleted theorem ordinal.div_le
deleted theorem ordinal.div_le_of_le_mul
deleted theorem ordinal.div_lt
deleted theorem ordinal.div_mul_cancel
deleted theorem ordinal.div_one
deleted theorem ordinal.div_self
deleted theorem ordinal.div_zero
deleted theorem ordinal.dvd_add
deleted theorem ordinal.dvd_add_iff
deleted theorem ordinal.dvd_antisymm
deleted theorem ordinal.dvd_def
deleted theorem ordinal.dvd_mul
deleted theorem ordinal.dvd_mul_of_dvd
deleted theorem ordinal.dvd_trans
deleted theorem ordinal.dvd_zero
deleted theorem ordinal.fintype_card
deleted theorem ordinal.is_limit.nat_lt
deleted theorem ordinal.is_limit.one_lt
deleted theorem ordinal.is_limit.pos
deleted def ordinal.is_limit
deleted theorem ordinal.is_limit_add_iff
deleted theorem ordinal.is_normal.bsup
deleted theorem ordinal.is_normal.bsup_eq
deleted theorem ordinal.is_normal.inj
deleted theorem ordinal.is_normal.le_iff
deleted theorem ordinal.is_normal.le_nfp
deleted theorem ordinal.is_normal.le_self
deleted theorem ordinal.is_normal.le_set'
deleted theorem ordinal.is_normal.le_set
deleted theorem ordinal.is_normal.lt_iff
deleted theorem ordinal.is_normal.lt_nfp
deleted theorem ordinal.is_normal.nfp_fp
deleted theorem ordinal.is_normal.nfp_le
deleted theorem ordinal.is_normal.refl
deleted theorem ordinal.is_normal.sup
deleted theorem ordinal.is_normal.trans
deleted def ordinal.is_normal
deleted theorem ordinal.iterate_le_nfp
deleted theorem ordinal.le_add_sub
deleted theorem ordinal.le_bsup
deleted theorem ordinal.le_div
deleted theorem ordinal.le_log
deleted theorem ordinal.le_nfp_self
deleted theorem ordinal.le_of_dvd
deleted theorem ordinal.le_power_self
deleted theorem ordinal.le_sup
deleted theorem ordinal.lift_add
deleted theorem ordinal.lift_is_limit
deleted theorem ordinal.lift_is_succ
deleted theorem ordinal.lift_mul
deleted theorem ordinal.lift_nat_cast
deleted theorem ordinal.lift_pred
deleted theorem ordinal.lift_succ
deleted theorem ordinal.lift_type_fin
deleted theorem ordinal.limit_le
deleted theorem ordinal.limit_rec_on_succ
deleted theorem ordinal.limit_rec_on_zero
deleted def ordinal.log
deleted theorem ordinal.log_def
deleted theorem ordinal.log_le_log
deleted theorem ordinal.log_le_self
deleted theorem ordinal.log_lt
deleted theorem ordinal.log_not_one_lt
deleted theorem ordinal.log_zero
deleted theorem ordinal.lt_bsup
deleted theorem ordinal.lt_div
deleted theorem ordinal.lt_limit
deleted theorem ordinal.lt_mul_div_add
deleted theorem ordinal.lt_mul_of_limit
deleted theorem ordinal.lt_mul_succ_div
deleted theorem ordinal.lt_omega
deleted theorem ordinal.lt_power_of_limit
deleted theorem ordinal.lt_power_succ_log
deleted theorem ordinal.lt_pred
deleted theorem ordinal.lt_sub
deleted theorem ordinal.lt_succ
deleted theorem ordinal.lt_sup
deleted theorem ordinal.mk_initial_seg
deleted theorem ordinal.mod_def
deleted theorem ordinal.mod_eq_of_lt
deleted theorem ordinal.mod_lt
deleted theorem ordinal.mod_one
deleted theorem ordinal.mod_self
deleted theorem ordinal.mod_zero
deleted theorem ordinal.mul_add
deleted theorem ordinal.mul_add_div
deleted theorem ordinal.mul_add_one
deleted theorem ordinal.mul_div_cancel
deleted theorem ordinal.mul_div_le
deleted theorem ordinal.mul_is_limit
deleted theorem ordinal.mul_is_limit_left
deleted theorem ordinal.mul_is_normal
deleted theorem ordinal.mul_le_mul
deleted theorem ordinal.mul_le_mul_left
deleted theorem ordinal.mul_le_mul_right
deleted theorem ordinal.mul_le_of_limit
deleted theorem ordinal.mul_lt_of_lt_div
deleted theorem ordinal.mul_lt_omega
deleted theorem ordinal.mul_ne_zero
deleted theorem ordinal.mul_omega
deleted theorem ordinal.mul_omega_dvd
deleted theorem ordinal.mul_pos
deleted theorem ordinal.mul_right_inj
deleted theorem ordinal.mul_sub
deleted theorem ordinal.mul_succ
deleted theorem ordinal.mul_zero
deleted theorem ordinal.nat_cast_div
deleted theorem ordinal.nat_cast_eq_zero
deleted theorem ordinal.nat_cast_inj
deleted theorem ordinal.nat_cast_le
deleted theorem ordinal.nat_cast_lt
deleted theorem ordinal.nat_cast_mod
deleted theorem ordinal.nat_cast_mul
deleted theorem ordinal.nat_cast_ne_zero
deleted theorem ordinal.nat_cast_pos
deleted theorem ordinal.nat_cast_power
deleted theorem ordinal.nat_cast_sub
deleted theorem ordinal.nat_cast_succ
deleted theorem ordinal.nat_le_card
deleted theorem ordinal.nat_lt_card
deleted theorem ordinal.nat_lt_limit
deleted theorem ordinal.nat_lt_omega
deleted def ordinal.nfp
deleted theorem ordinal.nfp_eq_self
deleted theorem ordinal.not_succ_is_limit
deleted theorem ordinal.not_zero_is_limit
deleted theorem ordinal.omega_is_limit
deleted theorem ordinal.omega_le
deleted theorem ordinal.omega_ne_zero
deleted theorem ordinal.omega_pos
deleted theorem ordinal.one_CNF
deleted theorem ordinal.one_add_omega
deleted theorem ordinal.one_dvd
deleted theorem ordinal.one_le_iff_pos
deleted theorem ordinal.one_lt_omega
deleted theorem ordinal.one_power
deleted def ordinal.power
deleted theorem ordinal.power_add
deleted theorem ordinal.power_dvd_power
deleted theorem ordinal.power_is_limit
deleted theorem ordinal.power_is_normal
deleted theorem ordinal.power_le_of_limit
deleted theorem ordinal.power_limit
deleted theorem ordinal.power_log_le
deleted theorem ordinal.power_lt_omega
deleted theorem ordinal.power_mul
deleted theorem ordinal.power_ne_zero
deleted theorem ordinal.power_omega
deleted theorem ordinal.power_one
deleted theorem ordinal.power_pos
deleted theorem ordinal.power_right_inj
deleted theorem ordinal.power_succ
deleted theorem ordinal.power_zero
deleted def ordinal.pred
deleted theorem ordinal.pred_le
deleted theorem ordinal.pred_le_self
deleted theorem ordinal.pred_succ
deleted def ordinal.sub
deleted theorem ordinal.sub_eq_of_add_eq
deleted theorem ordinal.sub_is_limit
deleted theorem ordinal.sub_le
deleted theorem ordinal.sub_le_self
deleted theorem ordinal.sub_self
deleted theorem ordinal.sub_sub
deleted theorem ordinal.sub_zero
deleted theorem ordinal.succ_inj
deleted theorem ordinal.succ_le_succ
deleted theorem ordinal.succ_log_def
deleted theorem ordinal.succ_lt_succ
deleted theorem ordinal.succ_ne_zero
deleted theorem ordinal.succ_pos
deleted theorem ordinal.succ_zero
deleted def ordinal.sup
deleted theorem ordinal.sup_le
deleted theorem ordinal.sup_ord
deleted theorem ordinal.sup_succ
deleted theorem ordinal.type_fin
deleted theorem ordinal.type_mul
deleted theorem ordinal.type_subrel_lt
deleted theorem ordinal.zero_CNF
deleted theorem ordinal.zero_div
deleted theorem ordinal.zero_dvd
deleted theorem ordinal.zero_lt_one
deleted theorem ordinal.zero_mod
deleted theorem ordinal.zero_mul
deleted theorem ordinal.zero_power'
deleted theorem ordinal.zero_power
deleted theorem ordinal.zero_sub
added theorem cardinal.ord_omega
added theorem ordinal.CNF_aux
added theorem ordinal.CNF_foldr
added theorem ordinal.CNF_fst_le
added theorem ordinal.CNF_fst_le_log
added theorem ordinal.CNF_ne_zero
added theorem ordinal.CNF_pairwise
added theorem ordinal.CNF_rec_zero
added theorem ordinal.CNF_snd_lt
added theorem ordinal.CNF_sorted
added theorem ordinal.CNF_zero
added theorem ordinal.add_absorp
added theorem ordinal.add_absorp_iff
added theorem ordinal.add_is_limit
added theorem ordinal.add_is_normal
added theorem ordinal.add_lt_omega
added theorem ordinal.add_mul_limit
added theorem ordinal.add_mul_succ
added theorem ordinal.add_omega
added theorem ordinal.add_sub_cancel
added theorem ordinal.add_succ
added def ordinal.bsup
added theorem ordinal.bsup_id
added theorem ordinal.bsup_le
added theorem ordinal.bsup_type
added theorem ordinal.card_eq_nat
added theorem ordinal.card_eq_zero
added theorem ordinal.card_le_nat
added theorem ordinal.card_lt_nat
added theorem ordinal.card_mul
added theorem ordinal.card_succ
added def ordinal.deriv
added theorem ordinal.deriv_limit
added theorem ordinal.deriv_succ
added theorem ordinal.deriv_zero
added theorem ordinal.div_add_mod
added theorem ordinal.div_def
added theorem ordinal.div_le
added theorem ordinal.div_lt
added theorem ordinal.div_mul_cancel
added theorem ordinal.div_one
added theorem ordinal.div_self
added theorem ordinal.div_zero
added theorem ordinal.dvd_add
added theorem ordinal.dvd_add_iff
added theorem ordinal.dvd_antisymm
added theorem ordinal.dvd_def
added theorem ordinal.dvd_mul
added theorem ordinal.dvd_mul_of_dvd
added theorem ordinal.dvd_trans
added theorem ordinal.dvd_zero
added theorem ordinal.fintype_card
added theorem ordinal.is_limit.pos
added def ordinal.is_limit
added theorem ordinal.is_normal.bsup
added theorem ordinal.is_normal.inj
added theorem ordinal.is_normal.refl
added theorem ordinal.is_normal.sup
added theorem ordinal.iterate_le_nfp
added theorem ordinal.le_add_sub
added theorem ordinal.le_bsup
added theorem ordinal.le_div
added theorem ordinal.le_log
added theorem ordinal.le_nfp_self
added theorem ordinal.le_of_dvd
added theorem ordinal.le_power_self
added theorem ordinal.le_sup
added theorem ordinal.lift_add
added theorem ordinal.lift_is_limit
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 theorem ordinal.lift_type_fin
added theorem ordinal.limit_le
added def ordinal.log
added theorem ordinal.log_def
added theorem ordinal.log_le_log
added theorem ordinal.log_le_self
added theorem ordinal.log_lt
added theorem ordinal.log_not_one_lt
added theorem ordinal.log_zero
added theorem ordinal.lt_bsup
added theorem ordinal.lt_div
added theorem ordinal.lt_limit
added theorem ordinal.lt_mul_div_add
added theorem ordinal.lt_omega
added theorem ordinal.lt_pred
added theorem ordinal.lt_sub
added theorem ordinal.lt_succ
added theorem ordinal.lt_sup
added theorem ordinal.mk_initial_seg
added theorem ordinal.mod_def
added theorem ordinal.mod_eq_of_lt
added theorem ordinal.mod_lt
added theorem ordinal.mod_one
added theorem ordinal.mod_self
added theorem ordinal.mod_zero
added theorem ordinal.mul_add
added theorem ordinal.mul_add_div
added theorem ordinal.mul_add_one
added theorem ordinal.mul_div_cancel
added theorem ordinal.mul_div_le
added theorem ordinal.mul_is_limit
added theorem ordinal.mul_is_normal
added theorem ordinal.mul_le_mul
added theorem ordinal.mul_lt_omega
added theorem ordinal.mul_ne_zero
added theorem ordinal.mul_omega
added theorem ordinal.mul_omega_dvd
added theorem ordinal.mul_pos
added theorem ordinal.mul_right_inj
added theorem ordinal.mul_sub
added theorem ordinal.mul_succ
added theorem ordinal.mul_zero
added theorem ordinal.nat_cast_div
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_pos
added theorem ordinal.nat_cast_power
added theorem ordinal.nat_cast_sub
added theorem ordinal.nat_cast_succ
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 def ordinal.nfp
added theorem ordinal.nfp_eq_self
added theorem ordinal.omega_is_limit
added theorem ordinal.omega_le
added theorem ordinal.omega_ne_zero
added theorem ordinal.omega_pos
added theorem ordinal.one_CNF
added theorem ordinal.one_add_omega
added theorem ordinal.one_dvd
added theorem ordinal.one_le_iff_pos
added theorem ordinal.one_lt_omega
added theorem ordinal.one_power
added def ordinal.power
added theorem ordinal.power_add
added theorem ordinal.power_is_limit
added theorem ordinal.power_limit
added theorem ordinal.power_log_le
added theorem ordinal.power_lt_omega
added theorem ordinal.power_mul
added theorem ordinal.power_ne_zero
added theorem ordinal.power_omega
added theorem ordinal.power_one
added theorem ordinal.power_pos
added theorem ordinal.power_succ
added theorem ordinal.power_zero
added def ordinal.pred
added theorem ordinal.pred_le
added theorem ordinal.pred_le_self
added theorem ordinal.pred_succ
added def ordinal.sub
added theorem ordinal.sub_is_limit
added theorem ordinal.sub_le
added theorem ordinal.sub_le_self
added theorem ordinal.sub_self
added theorem ordinal.sub_sub
added theorem ordinal.sub_zero
added theorem ordinal.succ_inj
added theorem ordinal.succ_le_succ
added theorem ordinal.succ_log_def
added theorem ordinal.succ_lt_succ
added theorem ordinal.succ_ne_zero
added theorem ordinal.succ_pos
added theorem ordinal.succ_zero
added def ordinal.sup
added theorem ordinal.sup_le
added theorem ordinal.sup_ord
added theorem ordinal.sup_succ
added theorem ordinal.type_fin
added theorem ordinal.type_mul
added theorem ordinal.type_subrel_lt
added theorem ordinal.zero_CNF
added theorem ordinal.zero_div
added theorem ordinal.zero_dvd
added theorem ordinal.zero_lt_one
added theorem ordinal.zero_mod
added theorem ordinal.zero_mul
added theorem ordinal.zero_power'
added theorem ordinal.zero_power
added theorem ordinal.zero_sub
modified def onote.NF
modified theorem onote.oadd_lt_oadd_1
modified theorem onote.oadd_lt_oadd_2
modified theorem onote.oadd_lt_oadd_3