infinite_of_left — Mathlib

English

If ι is infinite and π is nontrivial, the function space ι → π is infinite.

Русский

Если ι бесконечен и π ненулевой, пространство функций ι → π бесконечно.

LaTeX

$$$\\operatorname{Infinite}(\\iota) \\land \\operatorname{Nontrivial}(\\pi) \\Rightarrow \\operatorname{Infinite}(\\iota \\to \\pi)$$$

Lean4

/-- Non-dependent version of `Pi.infinite_of_left`. -/
instance infinite_of_left {ι : Sort*} {π : Type*} [Nontrivial π] [Infinite ι] : Infinite (ι → π) :=
  Pi.infinite_of_left

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