Commit 2024-10-03 10:05 23761ebb

View on Github →

refactor(SetTheory/Ordinal/Basic): deprecate Ordinal.omega in favor of Ordinal.omega0 (#17158) See zulip for the discussion.

Estimated changes

added theorem Ordinal.cof_omega0
deleted theorem Ordinal.cof_omega
added theorem Cardinal.aleph'_omega0
deleted theorem Cardinal.aleph'_omega
modified theorem Cardinal.aleph0_le_aleph'
modified theorem Cardinal.aleph_zero
deleted theorem Ordinal.omega_lt_omega1
added theorem Ordinal.lt_omega0
deleted theorem Ordinal.lt_omega
added theorem Ordinal.nat_lt_omega0
deleted theorem Ordinal.nat_lt_omega
added theorem Ordinal.omega0_isLimit
added theorem Ordinal.omega0_le
added theorem Ordinal.omega0_ne_zero
added theorem Ordinal.omega0_pos
deleted theorem Ordinal.omega_isLimit
deleted theorem Ordinal.omega_le
deleted theorem Ordinal.omega_ne_zero
added theorem Ordinal.one_add_omega0
deleted theorem Ordinal.one_add_omega
added theorem Ordinal.one_lt_omega0
deleted theorem Ordinal.one_lt_omega
added theorem Ordinal.card_omega0
deleted theorem Ordinal.card_omega
added theorem Ordinal.lift_omega0
deleted theorem Ordinal.lift_omega
added def Ordinal.omega0
deleted def Ordinal.omega
modified theorem Ordinal.nfp_add_zero
modified theorem Ordinal.nfp_mul_one
added theorem ONote.NF.of_dvd_omega0
deleted theorem ONote.NF.of_dvd_omega
added theorem ONote.omega0_le_oadd
deleted theorem ONote.omega_le_oadd
added theorem Ordinal.add_omega0
deleted theorem Ordinal.add_omega
deleted theorem Ordinal.add_omega_opow
deleted theorem Ordinal.mul_lt_omega_opow
added theorem Ordinal.mul_omega0
added theorem Ordinal.mul_omega0_dvd
deleted theorem Ordinal.mul_omega
deleted theorem Ordinal.mul_omega_dvd
added theorem Ordinal.opow_omega0
deleted theorem Ordinal.opow_omega