card_fun — Mathlib

English

If α is finite, then Nat.card (α → β) = Nat.card β ^ Nat.card α.

Русский

Если α конечно, то Nat.card(α → β) = Nat.card β в степени Nat.card α.

LaTeX

$$$$ Nat.card(\alpha \to \beta) = Nat.card(\beta)^{Nat.card(\alpha)} $$$$

Lean4

theorem card_fun [Finite α] : Nat.card (α → β) = Nat.card β ^ Nat.card α :=
  by
  haveI := Fintype.ofFinite α
  rw [Nat.card_pi, Finset.prod_const, Finset.card_univ, ← Nat.card_eq_fintype_card]

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