card_withConstants — Mathlib

English

The card of the language L with constants α is equal to lift(card of L) plus lift(#α) with appropriate universes.

Русский

Кардинал языка L с константами α равен подъему кардинала L плюс подъём кардинала α.

LaTeX

$$$ \\operatorname{card}(L[[\\alpha]]) = \\operatorname{lift}^{w'}(\\operatorname{card} L) + \\operatorname{lift}^{\\max(u,v)}(#\\alpha) $$$

Lean4

@[simp]
theorem card_withConstants : L[[α]].card = Cardinal.lift.{w'} L.card + Cardinal.lift.{max u v} #α := by
  rw [withConstants, card_sum, card_constantsOn]

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