card_relations_sum — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem card_relations_sum (i : ℕ) :
    #((L.sum L').Relations i) = Cardinal.lift.{v'} #(L.Relations i) + Cardinal.lift.{v} #(L'.Relations i) := by
  simp [Language.sum]

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