infinite_of_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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