Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-31 16:53 1bc2ac7a

View on Github →

feat(data/ordinal): is_normal, omin, power/log, CNF, indecomposables, addition and multiplication of infinite cardinals

Estimated changes

added theorem cardinal.add_le_add
added theorem cardinal.add_lt_omega
deleted theorem cardinal.add_mono
added theorem cardinal.le_add_left
added theorem cardinal.le_add_right
modified theorem cardinal.le_iff_exists_add
modified theorem cardinal.le_zero
added theorem cardinal.mul_le_mul
added theorem cardinal.mul_lt_omega
deleted theorem cardinal.mul_mono
added theorem cardinal.omega_le
added theorem cardinal.one_lt_omega
deleted theorem cardinal.power_mono_left
deleted theorem cardinal.power_mono_right
modified theorem cardinal.zero_le
added theorem cardinal.add_eq_max
added theorem cardinal.add_eq_self
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_le
added theorem cardinal.aleph_lt
added theorem cardinal.aleph_succ
added theorem cardinal.aleph_zero
added theorem cardinal.exists_aleph
added theorem cardinal.mul_eq_max
added theorem cardinal.mul_eq_self
added theorem cardinal.ord_card_le
added def cof
added def ordinal.CNF
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
modified theorem ordinal.add_is_limit
added theorem ordinal.add_is_normal
modified theorem ordinal.add_le_add_iff_left
modified theorem ordinal.add_le_add_left
added theorem ordinal.add_lt_omega
added theorem ordinal.add_omega
deleted def ordinal.aleph'
deleted theorem ordinal.aleph'_aleph_idx
deleted theorem ordinal.aleph'_le
deleted theorem ordinal.aleph'_lt
deleted theorem ordinal.aleph'_succ
deleted def ordinal.aleph
deleted theorem ordinal.aleph_idx_aleph'
deleted def ordinal.cof
added theorem ordinal.cof_sup_le
added theorem ordinal.is_limit.pos
added theorem ordinal.is_normal.inj
added theorem ordinal.is_normal.refl
modified theorem ordinal.le_add_right
added theorem ordinal.le_log
added theorem ordinal.le_omin
added theorem ordinal.le_power_self
modified theorem ordinal.le_sup
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.mul_add_one
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
modified theorem ordinal.mul_succ
added theorem ordinal.nat_cast_div
added theorem ordinal.nat_cast_mod
added theorem ordinal.nat_cast_mul
added theorem ordinal.nat_cast_power
added theorem ordinal.nat_cast_sub
added theorem ordinal.omega_ne_zero
added theorem ordinal.omega_pos
added def ordinal.omin
added theorem ordinal.omin_le
added theorem ordinal.omin_mem
added theorem ordinal.one_CNF
added theorem ordinal.one_le_iff_pos
added theorem ordinal.one_lt_omega
added theorem ordinal.one_power
deleted theorem ordinal.ord_card_le
deleted theorem ordinal.pos_of_is_limit
added theorem ordinal.power_add
added theorem ordinal.power_is_limit
modified theorem ordinal.power_le_of_limit
modified theorem ordinal.power_limit
added theorem ordinal.power_log_le
added theorem ordinal.power_mul
added theorem ordinal.power_ne_zero
added theorem ordinal.power_one
added theorem ordinal.power_pos
modified theorem ordinal.power_succ
modified theorem ordinal.power_zero
modified theorem ordinal.succ_le
added theorem ordinal.succ_log_def
modified theorem ordinal.succ_ne_zero
added theorem ordinal.succ_pos
added theorem ordinal.zero_CNF
added theorem ordinal.zero_lt_one
added theorem ordinal.zero_power'
added theorem ordinal.zero_power
modified theorem set.compl_image_set_of
modified theorem set.diff_diff
modified theorem set.diff_empty
modified theorem set.diff_neq_empty
modified theorem set.diff_right_antimono
modified theorem set.diff_subset_diff
modified theorem set.empty_prod
modified theorem set.forall_range_iff
modified theorem set.image_inter
modified theorem set.image_inter_on
modified theorem set.image_singleton
modified theorem set.image_swap_prod
modified theorem set.insert_prod
modified theorem set.insert_subset
modified theorem set.insert_subset_insert
modified theorem set.insert_union
modified theorem set.inter_assoc
modified theorem set.inter_comm
modified theorem set.inter_left_comm
modified theorem set.mem_image_of_injective
modified theorem set.mem_of_mem_of_subset
modified theorem set.mem_prod
modified theorem set.mem_prod_eq
modified theorem set.mem_range
modified theorem set.mem_range_self
modified theorem set.ne_empty_iff_exists_mem
modified theorem set.not_eq_empty_iff_exists
modified theorem set.not_not_mem
modified theorem set.not_subset
modified theorem set.prod_empty
modified theorem set.prod_image_image_eq
modified theorem set.prod_insert
modified theorem set.prod_inter_prod
modified theorem set.prod_mk_mem_set_prod_eq
modified theorem set.prod_mono
modified theorem set.prod_neq_empty_iff
modified theorem set.quot_mk_image_univ_eq
modified theorem set.range_compose
modified theorem set.range_eq_image
modified theorem set.range_id
modified theorem set.range_iff_surjective
modified theorem set.set_of_mem_eq
modified theorem set.union_assoc
modified theorem set.union_comm
modified theorem set.union_insert
deleted theorem set.union_insert_eq
modified theorem set.union_left_comm
added theorem set.union_singleton
modified theorem set.univ_eq_true_false
modified theorem set.univ_prod_univ