Library ▹ Essentials ▹ Numbers ▹ Cardinal numbers
Definition 1.8.2.12.  Let κ, μ be cardinal numbers. We define
κ + μ
by:
|K| + |J| := |K ⊎ J|  (K is a set, J is a set)
References.
  • https://en.wikipedia.org/wiki/Cardinal_number#Cardinal_addition
  • https://mathworld.wolfram.com/CardinalAddition.html
  • https://proofwiki.org/wiki/Definition:Sum_of_Cardinals
  • https://leanprover-community.github.io/mathlib_docs/set_theory/cardinal.html#cardinal.add_def
[View Source]