sum.slate

%../../../../../logics/hlm%

/**
 * @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
 */
$sum(κ,μ: %Element($"Cardinal numbers")): %ExplicitOperator {
  notation = $AdditionOperator(operands = [κ, μ]),
  definition = [%structuralCases(
    μ, $"Cardinal numbers",
    [{
      constructor = $"Cardinal numbers".cardinality,
      parameters = #(J: %Set),
      value = %structuralCases(
        κ, $"Cardinal numbers",
        [{
          constructor = $"Cardinal numbers".cardinality,
          parameters = #(K: %Set),
          value = $"Cardinal numbers".cardinality(S = $../../Sets/"Disjoint union"(S = K, T = J))
        }]
      )
    }]
  )]
}