Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-05 07:36 b6395b3a

View on Github →

refactor(set_theory/*): change omega to aleph_0 + golf (#14467) This PR does two things:

  • we change cardinal.omega to cardinal.aleph_0 and introduce the notation ℵ₀.
  • we golf many proofs throughout

Estimated changes

modified theorem cardinal.mk_rat
deleted theorem module.free.rank_lt_omega
deleted theorem cardinal.add_le_omega
deleted theorem cardinal.add_lt_omega
deleted theorem cardinal.add_lt_omega_iff
added def cardinal.aleph_0
added theorem cardinal.aleph_0_le
added theorem cardinal.aleph_0_le_mk
added theorem cardinal.aleph_0_pos
modified theorem cardinal.card_le_of
modified theorem cardinal.card_le_of_finset
modified theorem cardinal.denumerable_iff
modified theorem cardinal.encodable_iff
modified theorem cardinal.infinite_iff
added theorem cardinal.lift_aleph_0
deleted theorem cardinal.lift_le_omega
deleted theorem cardinal.lift_omega
added theorem cardinal.lt_aleph_0
deleted theorem cardinal.lt_omega
modified theorem cardinal.mk_denumerable
modified theorem cardinal.mk_int
added theorem cardinal.mk_le_aleph_0
deleted theorem cardinal.mk_le_omega
modified theorem cardinal.mk_nat
modified theorem cardinal.mk_pnat
deleted theorem cardinal.mk_set_le_omega
deleted theorem cardinal.mul_lt_omega
deleted theorem cardinal.mul_lt_omega_iff
deleted theorem cardinal.nat_lt_omega
deleted def cardinal.omega
deleted theorem cardinal.omega_add_omega
deleted theorem cardinal.omega_le
deleted theorem cardinal.omega_le_add_iff
deleted theorem cardinal.omega_le_lift
deleted theorem cardinal.omega_le_mk
deleted theorem cardinal.omega_le_mul_iff
deleted theorem cardinal.omega_mul_omega
deleted theorem cardinal.omega_ne_zero
deleted theorem cardinal.omega_pos
deleted theorem cardinal.one_lt_omega
modified theorem cardinal.one_to_nat
deleted theorem cardinal.power_lt_omega
modified theorem cardinal.to_enat_cast
modified theorem cardinal.to_nat_cast
modified theorem cardinal.zero_to_nat
modified theorem cardinal.deriv_lt_ord
modified theorem cardinal.is_inaccessible.mk
deleted theorem cardinal.is_limit_omega
deleted theorem cardinal.is_regular_omega
modified theorem cardinal.is_regular_succ
modified theorem cardinal.lt_cof_power
modified theorem cardinal.lt_power_cof
added theorem ordinal.aleph_0_le_cof
modified theorem ordinal.cof_omega
modified theorem ordinal.infinite_pigeonhole
modified theorem ordinal.nfp_bfamily_lt_ord
modified theorem ordinal.nfp_family_lt_ord
modified theorem ordinal.nfp_lt_ord
deleted theorem ordinal.omega_le_cof
modified def cardinal.continuum
modified theorem cardinal.continuum_mul_nat
modified theorem cardinal.lift_continuum
modified theorem cardinal.nat_lt_continuum
modified theorem cardinal.nat_mul_continuum
deleted theorem cardinal.nat_power_omega
deleted theorem cardinal.two_power_omega
modified theorem cardinal.is_prime_iff
modified theorem cardinal.is_prime_pow_iff
modified theorem cardinal.add_eq_left
modified theorem cardinal.add_eq_left_iff
modified theorem cardinal.add_eq_max'
modified theorem cardinal.add_eq_max
modified theorem cardinal.add_eq_right
modified theorem cardinal.add_eq_right_iff
modified theorem cardinal.add_eq_self
modified theorem cardinal.add_le_max
modified theorem cardinal.add_le_of_le
modified theorem cardinal.add_lt_of_lt
modified theorem cardinal.add_one_eq
modified theorem cardinal.aleph'_aleph_idx
modified theorem cardinal.aleph'_le
modified theorem cardinal.aleph'_le_of_limit
modified theorem cardinal.aleph'_lt
modified theorem cardinal.aleph'_omega
modified theorem cardinal.aleph'_succ
modified def cardinal.aleph
modified theorem cardinal.aleph_idx_aleph'
modified theorem cardinal.aleph_le
modified theorem cardinal.aleph_lt
deleted theorem cardinal.aleph_mul_omega
modified theorem cardinal.aleph_succ
modified theorem cardinal.aleph_zero
modified theorem cardinal.bit0_eq_self
modified theorem cardinal.bit0_lt_bit1
deleted theorem cardinal.bit0_lt_omega
modified theorem cardinal.bit1_eq_self_iff
modified theorem cardinal.bit1_le_bit0
deleted theorem cardinal.bit1_lt_omega
modified theorem cardinal.exists_aleph
deleted theorem cardinal.mk_list_eq_omega
modified theorem cardinal.mk_list_le_max
deleted theorem cardinal.mk_mul_omega_eq
modified theorem cardinal.mul_eq_left
modified theorem cardinal.mul_eq_left_iff
modified theorem cardinal.mul_eq_max'
modified theorem cardinal.mul_eq_max
modified theorem cardinal.mul_eq_right
modified theorem cardinal.mul_eq_self
modified theorem cardinal.mul_le_max
modified theorem cardinal.mul_lt_of_lt
deleted theorem cardinal.mul_omega_eq
modified theorem cardinal.nat_power_eq
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.omega_mul_aleph
deleted theorem cardinal.omega_mul_eq
deleted theorem cardinal.omega_mul_mk_eq
deleted theorem cardinal.one_le_one
modified theorem cardinal.ord_is_limit
modified theorem cardinal.pow_eq
modified theorem cardinal.pow_le
modified theorem cardinal.power_eq_two_power
modified theorem cardinal.power_nat_eq
modified theorem cardinal.power_nat_le
modified theorem cardinal.power_nat_le_max
modified theorem cardinal.power_self_eq
deleted theorem cardinal.powerlt_omega
deleted theorem cardinal.powerlt_omega_le
modified theorem cardinal.principal_add_ord
added theorem cardinal.succ_aleph_0
deleted theorem cardinal.succ_omega
modified theorem cardinal.type_cardinal
added theorem cardinal.ord_aleph_0
deleted theorem cardinal.ord_omega
modified theorem ordinal.add_le_of_limit
modified theorem ordinal.div_nonempty
modified theorem ordinal.lt_mul_of_limit
modified theorem ordinal.lt_omega
modified theorem ordinal.mul_le_of_limit
modified theorem ordinal.nat_lt_limit
modified theorem ordinal.nat_lt_omega
modified theorem ordinal.omega_is_limit
modified theorem ordinal.omega_le
modified theorem ordinal.omega_ne_zero
modified theorem ordinal.omega_pos
modified theorem ordinal.one_add_of_omega_le
modified theorem ordinal.one_add_omega
modified theorem ordinal.one_lt_omega
modified def ordinal.pred
modified theorem ordinal.sub_nonempty
modified theorem ordinal.sup_add_nat
modified theorem ordinal.sup_mul_nat
modified theorem ordinal.sup_nat_cast
modified theorem ordinal.sup_opow_nat
modified theorem cardinal.mk_ordinal_out
modified theorem ordinal.card_omega
modified theorem ordinal.lift_omega
modified def ordinal.univ
modified theorem ordinal.univ_id
modified theorem onote.repr_opow_aux₁