Commit 2023-02-11 10:18 f805dd1a

View on Github →

feat: port SetTheory.Cardinal.Basic (#2084)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Fintype/Option.lean

Created Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.add_def

added theorem Cardinal.add_le_aleph0

added theorem Cardinal.add_lt_aleph0

added theorem Cardinal.add_lt_aleph0_iff

added theorem Cardinal.add_one_le_succ

added def Cardinal.aleph0

added theorem Cardinal.aleph0_add_aleph0

added theorem Cardinal.aleph0_add_nat

added theorem Cardinal.aleph0_le

added theorem Cardinal.aleph0_le_add_iff

added theorem Cardinal.aleph0_le_lift

added theorem Cardinal.aleph0_le_mk

added theorem Cardinal.aleph0_le_mul_iff'

added theorem Cardinal.aleph0_le_mul_iff

added theorem Cardinal.aleph0_mul_aleph0

added theorem Cardinal.aleph0_mul_nat

added theorem Cardinal.aleph0_ne_zero

added theorem Cardinal.aleph0_pos

added theorem Cardinal.aleph0_toNat

added theorem Cardinal.aleph0_toPartENat

added theorem Cardinal.bddAbove_iff_small

added theorem Cardinal.bddAbove_image

added theorem Cardinal.bddAbove_of_small

added theorem Cardinal.bddAbove_range

added theorem Cardinal.bddAbove_range_comp

added theorem Cardinal.cantor'

added theorem Cardinal.cantor

added theorem Cardinal.card_le_of

added theorem Cardinal.card_le_of_finset

added theorem Cardinal.cast_toNat_of_aleph0_le

added theorem Cardinal.cast_toNat_of_lt_aleph0

added theorem Cardinal.denumerable_iff

added theorem Cardinal.eq_one_iff_unique

added theorem Cardinal.exists_nat_eq_of_le_nat

added theorem Cardinal.exists_not_mem_of_length_lt

added theorem Cardinal.finset_card_lt_aleph0

added theorem Cardinal.inductionOn

added theorem Cardinal.inductionOn₂

added theorem Cardinal.inductionOn₃

added theorem Cardinal.infinite_iff

added theorem Cardinal.infₛ_empty

added theorem Cardinal.le_aleph0_iff_set_countable

added theorem Cardinal.le_aleph0_iff_subtype_countable

added theorem Cardinal.le_def

added theorem Cardinal.le_lift_iff

added theorem Cardinal.le_mk_diff_add_mk

added theorem Cardinal.le_mk_iff_exists_set

added theorem Cardinal.le_mk_iff_exists_subset

added theorem Cardinal.le_one_iff_subsingleton

added theorem Cardinal.le_powerlt

added theorem Cardinal.le_sum

added def Cardinal.lift

added def Cardinal.liftOrderEmbedding

added theorem Cardinal.lift_add

added theorem Cardinal.lift_aleph0

added theorem Cardinal.lift_bit0

added theorem Cardinal.lift_bit1

added theorem Cardinal.lift_down

added theorem Cardinal.lift_eq_nat_iff

added theorem Cardinal.lift_eq_zero

added theorem Cardinal.lift_id'

added theorem Cardinal.lift_id

added theorem Cardinal.lift_infᵢ

added theorem Cardinal.lift_infₛ

added theorem Cardinal.lift_inj

added theorem Cardinal.lift_injective

added theorem Cardinal.lift_le

added theorem Cardinal.lift_le_aleph0

added theorem Cardinal.lift_lift

added theorem Cardinal.lift_lt

added theorem Cardinal.lift_max

added theorem Cardinal.lift_min

added theorem Cardinal.lift_mk_eq'

added theorem Cardinal.lift_mk_eq

added theorem Cardinal.lift_mk_fin

added theorem Cardinal.lift_mk_le'

added theorem Cardinal.lift_mk_le

added theorem Cardinal.lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le

added theorem Cardinal.lift_mk_shrink''

added theorem Cardinal.lift_mk_shrink'

added theorem Cardinal.lift_mk_shrink

added theorem Cardinal.lift_monotone

added theorem Cardinal.lift_mul

added theorem Cardinal.lift_natCast

added theorem Cardinal.lift_one

added theorem Cardinal.lift_power

added theorem Cardinal.lift_prod

added theorem Cardinal.lift_strictMono

added theorem Cardinal.lift_succ

added theorem Cardinal.lift_sum

added theorem Cardinal.lift_supᵢ

added theorem Cardinal.lift_supᵢ_le

added theorem Cardinal.lift_supᵢ_le_iff

added theorem Cardinal.lift_supᵢ_le_lift_supᵢ'

added theorem Cardinal.lift_supᵢ_le_lift_supᵢ

added theorem Cardinal.lift_supₛ

added theorem Cardinal.lift_two

added theorem Cardinal.lift_two_power

added theorem Cardinal.lift_umax'

added theorem Cardinal.lift_umax

added theorem Cardinal.lift_umax_eq

added theorem Cardinal.lift_uzero

added theorem Cardinal.lift_zero

added theorem Cardinal.lt_aleph0

added theorem Cardinal.lt_aleph0_iff_finite

added theorem Cardinal.lt_aleph0_iff_fintype

added theorem Cardinal.lt_aleph0_iff_set_finite

added theorem Cardinal.lt_aleph0_iff_subtype_finite

added theorem Cardinal.lt_aleph0_of_finite

added theorem Cardinal.lt_lift_iff

added def Cardinal.map

added theorem Cardinal.map_mk

added def Cardinal.map₂

added theorem Cardinal.mk'_def

added def Cardinal.mk

added theorem Cardinal.mk_Prop

added theorem Cardinal.mk_arrow

added theorem Cardinal.mk_bool

added theorem Cardinal.mk_bunionᵢ_le

added theorem Cardinal.mk_coe_finset

added theorem Cardinal.mk_congr

added theorem Cardinal.mk_denumerable

added theorem Cardinal.mk_diff_add_mk

added theorem Cardinal.mk_empty

added theorem Cardinal.mk_emptyCollection

added theorem Cardinal.mk_emptyCollection_iff

added theorem Cardinal.mk_eq_aleph0

added theorem Cardinal.mk_eq_nat_iff

added theorem Cardinal.mk_eq_nat_iff_finset

added theorem Cardinal.mk_eq_nat_iff_fintype

added theorem Cardinal.mk_eq_one

added theorem Cardinal.mk_eq_two_iff'

added theorem Cardinal.mk_eq_two_iff

added theorem Cardinal.mk_eq_zero

added theorem Cardinal.mk_eq_zero_iff

added theorem Cardinal.mk_fin

added theorem Cardinal.mk_finset_of_fintype

added theorem Cardinal.mk_finsupp_lift_of_fintype

added theorem Cardinal.mk_finsupp_of_fintype

added theorem Cardinal.mk_fintype

added theorem Cardinal.mk_image_eq

added theorem Cardinal.mk_image_eq_lift

added theorem Cardinal.mk_image_eq_of_injOn

added theorem Cardinal.mk_image_eq_of_injOn_lift

added theorem Cardinal.mk_image_le

added theorem Cardinal.mk_image_le_lift

added theorem Cardinal.mk_insert

added theorem Cardinal.mk_int

added theorem Cardinal.mk_le_aleph0

added theorem Cardinal.mk_le_aleph0_iff

added theorem Cardinal.mk_le_mk_mul_of_mk_preimage_le

added theorem Cardinal.mk_le_mk_of_subset

added theorem Cardinal.mk_le_of_injective

added theorem Cardinal.mk_le_of_surjective

added theorem Cardinal.mk_le_one_iff_set_subsingleton

added theorem Cardinal.mk_list_eq_sum_pow

added theorem Cardinal.mk_nat

added theorem Cardinal.mk_ne_zero

added theorem Cardinal.mk_ne_zero_iff

added theorem Cardinal.mk_option

added theorem Cardinal.mk_out

added theorem Cardinal.mk_pEmpty

added theorem Cardinal.mk_pLift_false

added theorem Cardinal.mk_pLift_true

added theorem Cardinal.mk_pNat

added theorem Cardinal.mk_pSum

added theorem Cardinal.mk_pUnit

added theorem Cardinal.mk_pi

added theorem Cardinal.mk_powerset

added theorem Cardinal.mk_preimage_of_injective

added theorem Cardinal.mk_preimage_of_injective_lift

added theorem Cardinal.mk_preimage_of_injective_of_subset_range

added theorem Cardinal.mk_preimage_of_injective_of_subset_range_lift

added theorem Cardinal.mk_preimage_of_subset_range

added theorem Cardinal.mk_preimage_of_subset_range_lift

added theorem Cardinal.mk_prod

added theorem Cardinal.mk_quot_le

added theorem Cardinal.mk_quotient_le

added theorem Cardinal.mk_range_eq

added theorem Cardinal.mk_range_eq_lift

added theorem Cardinal.mk_range_eq_of_injective

added theorem Cardinal.mk_range_le

added theorem Cardinal.mk_range_le_lift

added theorem Cardinal.mk_sep

added theorem Cardinal.mk_set

added theorem Cardinal.mk_set_eq_nat_iff_finset

added theorem Cardinal.mk_set_le

added theorem Cardinal.mk_sigma

added theorem Cardinal.mk_singleton

added theorem Cardinal.mk_subset_ge_of_subset_image

added theorem Cardinal.mk_subset_ge_of_subset_image_lift

added theorem Cardinal.mk_subtype_le

added theorem Cardinal.mk_subtype_le_of_subset

added theorem Cardinal.mk_subtype_mono

added theorem Cardinal.mk_subtype_of_equiv

added theorem Cardinal.mk_sum

added theorem Cardinal.mk_sum_compl

added theorem Cardinal.mk_toNat_eq_card

added theorem Cardinal.mk_toNat_of_infinite

added theorem Cardinal.mk_toPartENat_eq_coe_card

added theorem Cardinal.mk_toPartENat_of_infinite

added theorem Cardinal.mk_uLift

added theorem Cardinal.mk_union_add_mk_inter

added theorem Cardinal.mk_union_le

added theorem Cardinal.mk_union_le_aleph0

added theorem Cardinal.mk_union_of_disjoint

added theorem Cardinal.mk_unionᵢ_eq_sum_mk

added theorem Cardinal.mk_unionᵢ_le

added theorem Cardinal.mk_unionᵢ_le_sum_mk

added theorem Cardinal.mk_unionₛ_le

added theorem Cardinal.mk_unit

added theorem Cardinal.mk_univ

added theorem Cardinal.mk_vector

added theorem Cardinal.mul_def

added theorem Cardinal.mul_lt_aleph0

added theorem Cardinal.mul_lt_aleph0_iff

added theorem Cardinal.mul_lt_aleph0_iff_of_ne_zero

added theorem Cardinal.mul_power

added theorem Cardinal.natCast_inj

added theorem Cardinal.natCast_injective

added theorem Cardinal.natCast_le

added theorem Cardinal.natCast_lt

added theorem Cardinal.natCast_pow

added theorem Cardinal.nat_add_aleph0

added theorem Cardinal.nat_eq_lift_iff

added theorem Cardinal.nat_lt_aleph0

added theorem Cardinal.nat_mul_aleph0

added theorem Cardinal.nat_succ

added theorem Cardinal.nsmul_lt_aleph0_iff

added theorem Cardinal.nsmul_lt_aleph0_iff_of_ne_zero

added theorem Cardinal.one_le_aleph0

added theorem Cardinal.one_le_iff_ne_zero

added theorem Cardinal.one_le_iff_pos

added theorem Cardinal.one_lt_aleph0

added theorem Cardinal.one_lt_iff_nontrivial

added theorem Cardinal.one_power

added theorem Cardinal.one_toNat

added def Cardinal.outMkEquiv

added theorem Cardinal.out_embedding

added theorem Cardinal.pow_cast_right

added theorem Cardinal.power_add

added theorem Cardinal.power_bit0

added theorem Cardinal.power_bit1

added theorem Cardinal.power_def

added theorem Cardinal.power_le_max_power_one

added theorem Cardinal.power_le_power_left

added theorem Cardinal.power_le_power_right

added theorem Cardinal.power_lt_aleph0

added theorem Cardinal.power_mul

added theorem Cardinal.power_ne_zero

added theorem Cardinal.power_one

added theorem Cardinal.power_pos

added theorem Cardinal.power_zero

added def Cardinal.powerlt

added theorem Cardinal.powerlt_le

added theorem Cardinal.powerlt_le_powerlt_left

added theorem Cardinal.powerlt_max

added theorem Cardinal.powerlt_min

added theorem Cardinal.powerlt_mono_left

added theorem Cardinal.powerlt_succ

added theorem Cardinal.powerlt_zero

added def Cardinal.prod

added theorem Cardinal.prod_const'

added theorem Cardinal.prod_const

added theorem Cardinal.prod_eq_of_fintype

added theorem Cardinal.prod_eq_zero

added theorem Cardinal.prod_le_prod

added theorem Cardinal.prod_ne_zero

added theorem Cardinal.range_natCast

added theorem Cardinal.self_le_power

added theorem Cardinal.succ_def

added theorem Cardinal.succ_ne_zero

added theorem Cardinal.succ_pos

added theorem Cardinal.succ_zero

added def Cardinal.sum

added theorem Cardinal.sum_add_distrib'

added theorem Cardinal.sum_add_distrib

added theorem Cardinal.sum_const'

added theorem Cardinal.sum_const

added theorem Cardinal.sum_le_sum

added theorem Cardinal.sum_le_supᵢ

added theorem Cardinal.sum_le_supᵢ_lift

added theorem Cardinal.sum_lt_prod

added theorem Cardinal.sum_nat_eq_add_sum_succ

added theorem Cardinal.supᵢ_le_sum

added theorem Cardinal.three_le

added def Cardinal.toNat

added def Cardinal.toNatHom

added theorem Cardinal.toNat_add_of_lt_aleph0

added theorem Cardinal.toNat_apply_of_aleph0_le

added theorem Cardinal.toNat_apply_of_lt_aleph0

added theorem Cardinal.toNat_cast

added theorem Cardinal.toNat_congr

added theorem Cardinal.toNat_eq_iff

added theorem Cardinal.toNat_eq_one

added theorem Cardinal.toNat_eq_one_iff_unique

added theorem Cardinal.toNat_finset_prod

added theorem Cardinal.toNat_le_iff_le_of_lt_aleph0

added theorem Cardinal.toNat_le_of_le_of_lt_aleph0

added theorem Cardinal.toNat_lift

added theorem Cardinal.toNat_lt_iff_lt_of_lt_aleph0

added theorem Cardinal.toNat_lt_of_lt_of_lt_aleph0

added theorem Cardinal.toNat_mul

added theorem Cardinal.toNat_rightInverse

added theorem Cardinal.toNat_surjective

added def Cardinal.toPartENat

added theorem Cardinal.toPartENat_apply_of_aleph0_le

added theorem Cardinal.toPartENat_apply_of_lt_aleph0

added theorem Cardinal.toPartENat_cast

added theorem Cardinal.toPartENat_surjective

added theorem Cardinal.two_le_iff'

added theorem Cardinal.two_le_iff

added theorem Cardinal.zero_power

added theorem Cardinal.zero_power_le

added theorem Cardinal.zero_powerlt

added theorem Cardinal.zero_toNat

added def Cardinal

added theorem Function.Embedding.cardinal_le