infinite_of_left — Mathlib

English

If α is infinite and β is nonempty, then the product α × β is infinite.

Русский

Если α бесконечно и β непусто, то произведение α × β бесконечно.

LaTeX

$$$ (\\operatorname{Infinite}(\\alpha) \\land \\operatorname{Nonempty}(\\beta)) \\Rightarrow \\operatorname{Infinite}(\\alpha \\times \\beta) $$$

Lean4

instance infinite_of_left [Infinite α] [Nonempty β] : Infinite (α × β) :=
  Infinite.of_surjective Prod.fst Prod.fst_surjective

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