Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-06 02:12 4341fff2

View on Github →

chore(set_theory/cardinal_ordinal): use notation ω (#10197)

Estimated changes

Modified src/set_theory/cardinal_ordinal.lean

modified theorem cardinal.add_eq_left

modified theorem cardinal.add_eq_left_iff

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_lt_of_lt

modified theorem cardinal.add_one_eq

modified theorem cardinal.aleph'_omega

modified theorem cardinal.aleph_zero

modified theorem cardinal.bit0_eq_self

modified theorem cardinal.bit0_lt_bit1

modified theorem cardinal.bit0_lt_omega

modified theorem cardinal.bit1_eq_self_iff

modified theorem cardinal.bit1_le_bit0

modified theorem cardinal.bit1_lt_omega

modified theorem cardinal.eq_of_add_eq_of_omega_le

modified theorem cardinal.exists_aleph

modified theorem cardinal.mk_bounded_set_le_of_omega_le

modified theorem cardinal.mk_compl_eq_mk_compl_finite_same

modified theorem cardinal.mk_compl_eq_mk_compl_infinite

modified theorem cardinal.mk_compl_finset_of_omega_le

modified theorem cardinal.mk_compl_of_omega_le

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_of_omega_le_left

modified theorem cardinal.mul_eq_right

modified theorem cardinal.mul_eq_self

modified theorem cardinal.mul_le_max_of_omega_le_left

modified theorem cardinal.mul_lt_of_lt

modified theorem cardinal.omega_le_aleph'

modified theorem cardinal.omega_le_aleph

modified theorem cardinal.omega_le_bit0

modified theorem cardinal.omega_le_bit1

modified theorem cardinal.ord_is_limit

modified theorem cardinal.powerlt_omega

modified theorem cardinal.powerlt_omega_le