mk_prod — Mathlib

English

The cardinality of the product type α × β equals the product of the lifted cardinals: |α × β| = lift(|α|) · lift(|β|).

Русский

Кардинал произведения типов α × β равен произведению подъёмов кардиналов: |α × β| = lift(|α|) · lift(|β|).

LaTeX

$$$|\alpha \times \beta| = \operatorname{lift}( |\alpha| ) \cdot \operatorname{lift}( |\beta| )$$$

Lean4

@[simp]
theorem mk_prod (α : Type u) (β : Type v) : #(α × β) = lift.{v, u} #α * lift.{u, v} #β :=
  mk_congr (Equiv.ulift.symm.prodCongr Equiv.ulift.symm)

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