infinite_of_right — Mathlib

English

If every π(i) is infinite and ι is nonempty, then the Pi-type ∀ i, π(i) is infinite.

Русский

Если каждый π(i) бесконечен и ι непуст, тогда Π i:ι π(i) бесконечно.

LaTeX

$$$(\\forall i:\\iota, \\operatorname{Infinite}(\\pi i)) \\land \\operatorname{Nonempty}(\\iota) \\Rightarrow \\operatorname{Infinite}(\\forall i:\\iota, \\pi i)$$$

Lean4

/-- See `Pi.infinite_of_exists_right` for the case that only one `π i` is infinite. -/
instance infinite_of_right {ι : Sort*} {π : ι → Type*} [∀ i, Infinite <| π i] [Nonempty ι] : Infinite (∀ i : ι, π i) :=
  Pi.infinite_of_exists_right (Classical.arbitrary ι)

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