pi' — Mathlib

English

If each t(i) is finite, then the set {f : ∀ i, κ i | ∀ i, f(i) ∈ t(i)} is finite.

Русский

Если для каждого i множество t(i) конечное, то множество функций f : ∀ i, κ(i) с условием f(i) ∈ t(i) для всех i конечно.

LaTeX

$$$\\operatorname{Finite}\\left(\\{ f : \\forall i, \\kappa(i) \\mid \\forall i, f(i) \\in t(i)\\} \\right).$$$

Lean4

/-- Finite product of finite sets is finite. Note this is a variant of `Set.Finite.pi` without the
extra `i ∈ univ` binder. -/
theorem pi' (ht : ∀ i, (t i).Finite) : {f : ∀ i, κ i | ∀ i, f i ∈ t i}.Finite := by simpa [Set.pi] using Finite.pi ht

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