card_eq_card_functions_add_card_relations

English

The cardinality of a language L is the sum of the lifted cardinalities of its function and relation symbols.

Русский

Мощность языка L равна сумме поднесённых мощностей его символь функций и отношений.

LaTeX

$$$|L| = \sum_{l} |L.Functions(l)| + \sum_{l} |L.Relations(l)|$$$

Lean4

theorem card_eq_card_functions_add_card_relations :
    L.card =
      (Cardinal.sum fun l => Cardinal.lift.{v} #(L.Functions l)) +
        Cardinal.sum fun l => Cardinal.lift.{u} #(L.Relations l) :=
  by simp only [card, mk_sum, mk_sigma, lift_sum]

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