card_functions_sum — Mathlib

English

For each i, the cardinality of the i-th function type in the sum language equals the lifted sum of the two component function types.

Русский

Для каждого i кардинальность типа функций i-й компоненты языка сумма равна поднесённой сумме соответствующих кардинал различных компонент.

LaTeX

$$$\lvert (L.sum L').Functions(i) \rvert = (\lvert L.Functions(i) \rvert)^{\uparrow} + (\lvert L'.Functions(i) \rvert)^{\uparrow}$$$

Lean4

@[simp]
theorem card_functions_sum (i : ℕ) :
    #((L.sum L').Functions i) =
      (Cardinal.lift.{u'} #(L.Functions i) + Cardinal.lift.{u} #(L'.Functions i) : Cardinal) :=
  by simp [Language.sum]

Похожие утверждения