mk_arrow — Mathlib

English

The cardinality of the function type α → β equals the lifted cardinal of β to the power of the lifted cardinal of α: |α → β| = (lift(|β|))^{lift(|α|)}.

Русский

Кардинал типа функций α → β равен возведению подъёмленного кардинала β в степень подъёмного кардинала α: |α → β| = (lift(|β|))^{lift(|α|)}.

LaTeX

$$$|\alpha \to \beta| = (\operatorname{lift}( |\beta| ))^{( \operatorname{lift}( |\alpha| )}$$$

Lean4

theorem mk_arrow (α : Type u) (β : Type v) : #(α → β) = (lift.{u} #β ^ lift.{v} #α) :=
  mk_congr (Equiv.ulift.symm.arrowCongr Equiv.ulift.symm)

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