mk_sigma_arrow — Mathlib

English

The cardinality of the type of functions from Sigma f to α equals the cardinality of the product of function types f i → α: |Sigma f → α| = |Π i, f i → α|.

Русский

Кардинал типа функций из сигмы в α равен кардиналу произведения функций f i → α: |Sigma f → α| = |Π i, f i → α|.

LaTeX

$$$|\Sigma f \to \alpha| = |\Pi i, f i \to \alpha|$$$

Lean4

theorem mk_sigma_arrow {ι} (α : Type*) (f : ι → Type*) : #(Sigma f → α) = #(Π i, f i → α) :=
  mk_congr <| Equiv.piCurry fun _ _ ↦ α

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