Commit 2023-02-23 13:50 1231af35

View on Github →

feat: port SetTheory.Cardinal.Ordinal (#2463)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

Created Mathlib/SetTheory/Cardinal/Ordinal.lean

added def Cardinal.Aleph'.relIso

added theorem Cardinal.add_eq_left

added theorem Cardinal.add_eq_left_iff

added theorem Cardinal.add_eq_max'

added theorem Cardinal.add_eq_max

added theorem Cardinal.add_eq_right

added theorem Cardinal.add_eq_right_iff

added theorem Cardinal.add_eq_self

added theorem Cardinal.add_le_add_iff_of_lt_aleph0

added theorem Cardinal.add_le_max

added theorem Cardinal.add_le_of_le

added theorem Cardinal.add_lt_of_lt

added theorem Cardinal.add_mk_eq_max'

added theorem Cardinal.add_mk_eq_max

added theorem Cardinal.add_nat_eq

added theorem Cardinal.add_nat_inj

added theorem Cardinal.add_nat_le_add_nat_iff_of_lt_aleph_0

added theorem Cardinal.add_one_eq

added theorem Cardinal.add_one_inj

added theorem Cardinal.add_one_le_add_one_iff_of_lt_aleph_0

added theorem Cardinal.add_right_inj_of_lt_aleph0

added theorem Cardinal.aleph'.relIso_coe

added def Cardinal.aleph'

added def Cardinal.aleph'Equiv

added theorem Cardinal.aleph'_alephIdx

added theorem Cardinal.aleph'_isNormal

added theorem Cardinal.aleph'_le

added theorem Cardinal.aleph'_le_of_limit

added theorem Cardinal.aleph'_limit

added theorem Cardinal.aleph'_lt

added theorem Cardinal.aleph'_nat

added theorem Cardinal.aleph'_omega

added theorem Cardinal.aleph'_pos

added theorem Cardinal.aleph'_succ

added theorem Cardinal.aleph'_zero

added theorem Cardinal.aleph0_le_aleph'

added theorem Cardinal.aleph0_le_aleph

added theorem Cardinal.aleph0_le_beth

added theorem Cardinal.aleph0_lt_aleph_one

added theorem Cardinal.aleph0_mul_aleph

added theorem Cardinal.aleph0_mul_eq

added theorem Cardinal.aleph0_mul_mk_eq

added def Cardinal.aleph

added theorem Cardinal.alephIdx.init

added def Cardinal.alephIdx.initialSeg

added theorem Cardinal.alephIdx.initialSeg_coe

added def Cardinal.alephIdx.relIso

added theorem Cardinal.alephIdx.relIso_coe

added def Cardinal.alephIdx

added theorem Cardinal.alephIdx_aleph'

added theorem Cardinal.alephIdx_le

added theorem Cardinal.alephIdx_lt

added theorem Cardinal.aleph_add_aleph

added theorem Cardinal.aleph_isNormal

added theorem Cardinal.aleph_le

added theorem Cardinal.aleph_le_beth

added theorem Cardinal.aleph_limit

added theorem Cardinal.aleph_lt

added theorem Cardinal.aleph_mul_aleph0

added theorem Cardinal.aleph_mul_aleph

added theorem Cardinal.aleph_pos

added theorem Cardinal.aleph_succ

added theorem Cardinal.aleph_toNat

added theorem Cardinal.aleph_toPartENat

added theorem Cardinal.aleph_zero

added def Cardinal.beth

added theorem Cardinal.beth_le

added theorem Cardinal.beth_limit

added theorem Cardinal.beth_lt

added theorem Cardinal.beth_mono

added theorem Cardinal.beth_ne_zero

added theorem Cardinal.beth_normal

added theorem Cardinal.beth_pos

added theorem Cardinal.beth_strictMono

added theorem Cardinal.beth_succ

added theorem Cardinal.beth_zero

added theorem Cardinal.countable_iff_lt_aleph_one

added theorem Cardinal.eq_aleph'_of_eq_card_ord

added theorem Cardinal.eq_aleph_of_eq_card_ord

added theorem Cardinal.eq_of_add_eq_of_aleph0_le

added theorem Cardinal.exists_aleph

added theorem Cardinal.extend_function

added theorem Cardinal.extend_function_finite

added theorem Cardinal.extend_function_of_lt

added theorem Cardinal.le_mul_left

added theorem Cardinal.le_mul_right

added theorem Cardinal.max_aleph_eq

added theorem Cardinal.mk_add_one_eq

added theorem Cardinal.mk_bounded_set_le

added theorem Cardinal.mk_bounded_set_le_of_infinite

added theorem Cardinal.mk_bounded_subset_le

added theorem Cardinal.mk_cardinal

added theorem Cardinal.mk_compl_eq_mk_compl_finite

added theorem Cardinal.mk_compl_eq_mk_compl_finite_lift

added theorem Cardinal.mk_compl_eq_mk_compl_finite_same

added theorem Cardinal.mk_compl_eq_mk_compl_infinite

added theorem Cardinal.mk_compl_finset_of_infinite

added theorem Cardinal.mk_compl_of_infinite

added theorem Cardinal.mk_finset_of_infinite

added theorem Cardinal.mk_finsupp_lift_of_infinite'

added theorem Cardinal.mk_finsupp_lift_of_infinite

added theorem Cardinal.mk_finsupp_nat

added theorem Cardinal.mk_finsupp_of_infinite'

added theorem Cardinal.mk_finsupp_of_infinite

added theorem Cardinal.mk_list_eq_aleph0

added theorem Cardinal.mk_list_eq_max_mk_aleph0

added theorem Cardinal.mk_list_eq_mk

added theorem Cardinal.mk_list_le_max

added theorem Cardinal.mk_mul_aleph0_eq

added theorem Cardinal.mk_multiset_of_countable

added theorem Cardinal.mk_multiset_of_infinite

added theorem Cardinal.mk_multiset_of_isEmpty

added theorem Cardinal.mk_multiset_of_nonempty

added theorem Cardinal.mul_aleph0_eq

added theorem Cardinal.mul_eq_left

added theorem Cardinal.mul_eq_left_iff

added theorem Cardinal.mul_eq_max'

added theorem Cardinal.mul_eq_max

added theorem Cardinal.mul_eq_max_of_aleph0_le_left

added theorem Cardinal.mul_eq_max_of_aleph0_le_right

added theorem Cardinal.mul_eq_right

added theorem Cardinal.mul_eq_self

added theorem Cardinal.mul_le_max

added theorem Cardinal.mul_le_max_of_aleph0_le_left

added theorem Cardinal.mul_le_max_of_aleph0_le_right

added theorem Cardinal.mul_lt_of_lt

added theorem Cardinal.mul_mk_eq_max

added theorem Cardinal.nat_power_eq

added theorem Cardinal.ord_aleph'_eq_enum_card

added theorem Cardinal.ord_aleph_eq_enum_card

added theorem Cardinal.ord_aleph_isLimit

added theorem Cardinal.ord_card_unbounded'

added theorem Cardinal.ord_card_unbounded

added theorem Cardinal.ord_isLimit

added theorem Cardinal.pow_eq

added theorem Cardinal.pow_le

added theorem Cardinal.power_eq_two_power

added theorem Cardinal.power_nat_eq

added theorem Cardinal.power_nat_le

added theorem Cardinal.power_nat_le_max

added theorem Cardinal.power_self_eq

added theorem Cardinal.powerlt_aleph0

added theorem Cardinal.powerlt_aleph0_le

added theorem Cardinal.principal_add_aleph

added theorem Cardinal.principal_add_ord

added theorem Cardinal.prod_eq_two_power

added theorem Cardinal.succ_aleph0

added theorem Cardinal.type_cardinal