mk_psum — Mathlib

English

Let α and β be types. The cardinality of the dependent sum PSum α β equals the sum of the lifted cardinals: |PSum α β| = lift(|α|) + lift(|β|).

Русский

Пусть α и β — типы. Кардинал зависимого суммирования PSum α β равен сумме подъёмов кардиналов: |PSum α β| = lift(|α|) + lift(|β|).

LaTeX

$$$|\mathrm{PSum}(\alpha, \beta)| = \operatorname{lift}( |\alpha| ) + \operatorname{lift}( |\beta| )$$$

Lean4

@[simp]
theorem mk_psum (α : Type u) (β : Type v) : #(α ⊕' β) = lift.{v} #α + lift.{u} #β :=
  (mk_congr (Equiv.psumEquivSum α β)).trans (mk_sum α β)

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