card_sum — Mathlib

English

The cardinality of the sum language equals the sum of the cardinalities of the two languages, up to lifting.

Русский

Мощность суммы языков равна сумме мощностей обоих языков, учитывая поднесение к соответствующей вселенной.

LaTeX

$$$|L.sum L'| = |L.card|^{\uparrow} + |L'.card|^{\uparrow}$$$

Lean4

theorem card_sum : (L.sum L').card = Cardinal.lift.{max u' v'} L.card + Cardinal.lift.{max u v} L'.card := by
  simp only [card, mk_sum, mk_sigma, card_functions_sum, sum_add_distrib', lift_add, lift_sum, lift_lift,
    card_relations_sum, add_assoc, add_comm (Cardinal.sum fun i => (#(L'.Functions i)).lift)]

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