Commit 2025-03-18 10:57 a80159d3

View on Github →

chore(SetTheory): split Cardinal/Basic.lean (#23014) This PR splits SetTheory.Cardinal.Basic into three files:

  • Cardinal/Defs.lean: definition of Cardinal, addition, zero, א0
  • Cardinal/Order.lean: definition of pre/linear/wellorder on Cardinal, semiring and ordered semiring structures
  • Cardinal/Basic.lean: leftovers, in particular finite/countable/small types and sets In particular, Defs.lean defines cardinals without importing any algebra (measured with an assert_not_exists Monoid). I would have liked to do more with Cardinal/Order.lean such as splitting it into a file focused more on the order and a file focused more on the arithmetic, but unfortunately the two are currently so interwoven that it would not make sense to break them apart. (It would require substantial redoing of proofs.) Even moving the Preorder Cardinal instance upstream is hard since it depends on Schröder-Bernstein which imports lots of algebra. It wouldn't actually help the imports much.

Estimated changes

deleted theorem Cardinal.IsLimit.succ_lt
deleted def Cardinal.IsLimit
deleted structure Cardinal.IsStrongLimit
deleted theorem Cardinal.add_def
deleted theorem Cardinal.add_one_le_succ
deleted def Cardinal.aleph0
deleted theorem Cardinal.aleph0_eq_lift
deleted theorem Cardinal.aleph0_le_lift
deleted theorem Cardinal.aleph0_lt_lift
deleted theorem Cardinal.aleph0_ne_zero
deleted theorem Cardinal.aleph0_pos
deleted theorem Cardinal.cantor
deleted theorem Cardinal.iSup_le_sum
deleted theorem Cardinal.inductionOn
deleted theorem Cardinal.inductionOn₂
deleted theorem Cardinal.inductionOn₃
deleted theorem Cardinal.induction_on_pi
deleted theorem Cardinal.le_def
deleted theorem Cardinal.le_lift_iff
deleted theorem Cardinal.le_sum
deleted def Cardinal.lift
deleted theorem Cardinal.lift_add
deleted theorem Cardinal.lift_aleph0
deleted theorem Cardinal.lift_down
deleted theorem Cardinal.lift_eq_aleph0
deleted theorem Cardinal.lift_eq_nat_iff
deleted theorem Cardinal.lift_eq_one
deleted theorem Cardinal.lift_eq_zero
deleted theorem Cardinal.lift_id'
deleted theorem Cardinal.lift_id
deleted theorem Cardinal.lift_inj
deleted theorem Cardinal.lift_injective
deleted theorem Cardinal.lift_le
deleted theorem Cardinal.lift_le_aleph0
deleted theorem Cardinal.lift_le_nat_iff
deleted theorem Cardinal.lift_le_one_iff
deleted theorem Cardinal.lift_lift.{u_1}
deleted theorem Cardinal.lift_lt
deleted theorem Cardinal.lift_lt_aleph0
deleted theorem Cardinal.lift_lt_nat_iff
deleted theorem Cardinal.lift_max
deleted theorem Cardinal.lift_min
deleted theorem Cardinal.lift_mk_eq'
deleted theorem Cardinal.lift_mk_eq
deleted theorem Cardinal.lift_mk_fin
deleted theorem Cardinal.lift_mk_le'
deleted theorem Cardinal.lift_mk_le
deleted theorem Cardinal.lift_monotone
deleted theorem Cardinal.lift_mul
deleted theorem Cardinal.lift_natCast
deleted theorem Cardinal.lift_ofNat
deleted theorem Cardinal.lift_one
deleted theorem Cardinal.lift_power
deleted theorem Cardinal.lift_prod
deleted theorem Cardinal.lift_strictMono
deleted theorem Cardinal.lift_succ
deleted theorem Cardinal.lift_sum
deleted theorem Cardinal.lift_two
deleted theorem Cardinal.lift_two_power
deleted theorem Cardinal.lift_umax'
deleted theorem Cardinal.lift_umax
deleted theorem Cardinal.lift_umax_eq
deleted theorem Cardinal.lift_uzero
deleted theorem Cardinal.lift_zero
deleted theorem Cardinal.lt_lift_iff
deleted def Cardinal.map
deleted theorem Cardinal.map_mk
deleted def Cardinal.map₂
deleted theorem Cardinal.mk'_def
deleted def Cardinal.mk
deleted theorem Cardinal.mk_Prop
deleted theorem Cardinal.mk_arrow
deleted theorem Cardinal.mk_bool
deleted theorem Cardinal.mk_coe_finset
deleted theorem Cardinal.mk_congr
deleted theorem Cardinal.mk_congr_lift
deleted theorem Cardinal.mk_empty
deleted theorem Cardinal.mk_eq_one
deleted theorem Cardinal.mk_eq_zero
deleted theorem Cardinal.mk_eq_zero_iff
deleted theorem Cardinal.mk_fin
deleted theorem Cardinal.mk_fintype
deleted theorem Cardinal.mk_nat
deleted theorem Cardinal.mk_ne_zero
deleted theorem Cardinal.mk_ne_zero_iff
deleted theorem Cardinal.mk_option
deleted theorem Cardinal.mk_out
deleted theorem Cardinal.mk_pempty
deleted theorem Cardinal.mk_pi
deleted theorem Cardinal.mk_pi_congr'
deleted theorem Cardinal.mk_pi_congr
deleted theorem Cardinal.mk_pi_congrRight
deleted theorem Cardinal.mk_pi_congr_lift
deleted theorem Cardinal.mk_pi_congr_prop
deleted theorem Cardinal.mk_plift_false
deleted theorem Cardinal.mk_plift_true
deleted theorem Cardinal.mk_powerset
deleted theorem Cardinal.mk_prod
deleted theorem Cardinal.mk_psum
deleted theorem Cardinal.mk_punit
deleted theorem Cardinal.mk_set
deleted theorem Cardinal.mk_set_le
deleted theorem Cardinal.mk_sigma
deleted theorem Cardinal.mk_sigma_arrow
deleted theorem Cardinal.mk_sigma_congr'
deleted theorem Cardinal.mk_sigma_congr
deleted theorem Cardinal.mk_subtype_le
deleted theorem Cardinal.mk_sum
deleted theorem Cardinal.mk_uLift
deleted theorem Cardinal.mk_unit
deleted theorem Cardinal.mul_def
deleted theorem Cardinal.mul_power
deleted theorem Cardinal.nat_eq_lift_iff
deleted theorem Cardinal.nat_le_lift_iff
deleted theorem Cardinal.nat_lt_lift_iff
deleted theorem Cardinal.one_eq_lift_iff
deleted theorem Cardinal.one_le_lift_iff
deleted theorem Cardinal.one_lt_lift_iff
deleted theorem Cardinal.one_power
deleted def Cardinal.outMkEquiv
deleted theorem Cardinal.out_embedding
deleted theorem Cardinal.out_lift_equiv
deleted theorem Cardinal.power_add
deleted theorem Cardinal.power_def
deleted theorem Cardinal.power_mul
deleted theorem Cardinal.power_natCast
deleted theorem Cardinal.power_ne_zero
deleted theorem Cardinal.power_one
deleted theorem Cardinal.power_pos
deleted theorem Cardinal.power_sum
deleted theorem Cardinal.power_zero
deleted def Cardinal.prod
deleted theorem Cardinal.prod_const'
deleted theorem Cardinal.prod_const
deleted theorem Cardinal.prod_eq_zero
deleted theorem Cardinal.prod_le_prod
deleted theorem Cardinal.prod_ne_zero
deleted theorem Cardinal.sInf_empty
deleted theorem Cardinal.self_le_power
deleted theorem Cardinal.succ_def
deleted theorem Cardinal.succ_ne_zero
deleted theorem Cardinal.succ_pos
deleted def Cardinal.sum
deleted theorem Cardinal.sum_add_distrib'
deleted theorem Cardinal.sum_add_distrib
deleted theorem Cardinal.sum_const'
deleted theorem Cardinal.sum_const
deleted theorem Cardinal.sum_le_sum
deleted theorem Cardinal.sum_lt_prod
deleted theorem Cardinal.zero_eq_lift_iff
deleted theorem Cardinal.zero_lt_lift_iff
deleted theorem Cardinal.zero_power
deleted theorem Cardinal.zero_power_le
deleted def Cardinal
deleted def WellOrderingRel
deleted def embeddingToCardinal
deleted theorem exists_wellOrder
added theorem Cardinal.add_def
added def Cardinal.aleph0
added theorem Cardinal.inductionOn
added def Cardinal.lift
added theorem Cardinal.lift_add
added theorem Cardinal.lift_aleph0
added theorem Cardinal.lift_id'
added theorem Cardinal.lift_id
added theorem Cardinal.lift_mk_eq'
added theorem Cardinal.lift_mk_eq
added theorem Cardinal.lift_mk_fin
added theorem Cardinal.lift_one
added theorem Cardinal.lift_power
added theorem Cardinal.lift_prod
added theorem Cardinal.lift_sum
added theorem Cardinal.lift_umax'
added theorem Cardinal.lift_umax
added theorem Cardinal.lift_uzero
added theorem Cardinal.lift_zero
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_arrow
added theorem Cardinal.mk_congr
added theorem Cardinal.mk_congr_lift
added theorem Cardinal.mk_empty
added theorem Cardinal.mk_eq_one
added theorem Cardinal.mk_eq_zero
added theorem Cardinal.mk_nat
added theorem Cardinal.mk_ne_zero
added theorem Cardinal.mk_option
added theorem Cardinal.mk_out
added theorem Cardinal.mk_pempty
added theorem Cardinal.mk_pi
added theorem Cardinal.mk_pi_congr'
added theorem Cardinal.mk_pi_congr
added theorem Cardinal.mk_plift_true
added theorem Cardinal.mk_prod
added theorem Cardinal.mk_psum
added theorem Cardinal.mk_punit
added theorem Cardinal.mk_sigma
added theorem Cardinal.mk_sum
added theorem Cardinal.mk_uLift
added theorem Cardinal.mk_unit
added theorem Cardinal.mul_def
added theorem Cardinal.mul_power
added theorem Cardinal.one_power
added theorem Cardinal.power_add
added theorem Cardinal.power_def
added theorem Cardinal.power_ne_zero
added theorem Cardinal.power_one
added theorem Cardinal.power_sum
added theorem Cardinal.power_zero
added def Cardinal.prod
added theorem Cardinal.prod_const'
added theorem Cardinal.prod_const
added theorem Cardinal.prod_eq_zero
added theorem Cardinal.prod_ne_zero
added def Cardinal.sum
added theorem Cardinal.sum_const'
added theorem Cardinal.sum_const
added theorem Cardinal.zero_power
added def Cardinal
added def Cardinal.IsLimit
added structure Cardinal.IsStrongLimit
added theorem Cardinal.aleph0_pos
added theorem Cardinal.cantor
added theorem Cardinal.iSup_le_sum
added theorem Cardinal.le_def
added theorem Cardinal.le_lift_iff
added theorem Cardinal.le_sum
added theorem Cardinal.lift_down
added theorem Cardinal.lift_eq_one
added theorem Cardinal.lift_eq_zero
added theorem Cardinal.lift_inj
added theorem Cardinal.lift_le
added theorem Cardinal.lift_lt
added theorem Cardinal.lift_max
added theorem Cardinal.lift_min
added theorem Cardinal.lift_mk_le'
added theorem Cardinal.lift_mk_le
added theorem Cardinal.lift_monotone
added theorem Cardinal.lift_mul
added theorem Cardinal.lift_natCast
added theorem Cardinal.lift_ofNat
added theorem Cardinal.lift_succ
added theorem Cardinal.lift_two
added theorem Cardinal.lift_umax_eq
added theorem Cardinal.lt_lift_iff
added theorem Cardinal.mk_Prop
added theorem Cardinal.mk_bool
added theorem Cardinal.mk_coe_finset
added theorem Cardinal.mk_fin
added theorem Cardinal.mk_fintype
added theorem Cardinal.mk_powerset
added theorem Cardinal.mk_set
added theorem Cardinal.mk_set_le
added theorem Cardinal.mk_subtype_le
added theorem Cardinal.out_embedding
added theorem Cardinal.power_mul
added theorem Cardinal.power_natCast
added theorem Cardinal.power_pos
added theorem Cardinal.prod_le_prod
added theorem Cardinal.sInf_empty
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.sum_le_sum
added theorem Cardinal.sum_lt_prod
added theorem Cardinal.zero_power_le
added def WellOrderingRel
added theorem exists_wellOrder