mk_sum — Mathlib

English

Let α and β be types. The cardinality of their disjoint sum equals the sum of their cardinals after lifting to a common universe: |α ⊕ β| = lift(|α|) + lift(|β|).

Русский

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

LaTeX

$$$|\alpha \oplus \beta| = \operatorname{lift}( |\alpha| ) + \operatorname{lift}( |\beta|)$$$

Lean4

@[simp]
theorem mk_sum (α : Type u) (β : Type v) : #(α ⊕ β) = lift.{v, u} #α + lift.{u, v} #β :=
  mk_congr (Equiv.ulift.symm.sumCongr Equiv.ulift.symm)

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