instSigmaOfNonempty_1 — Mathlib

English

If α is nonempty and every fiber β(a) is infinite, then the sigma-type ∑ a: α, β(a) is infinite.

Русский

Если α непусто и каждый β(a) бесконечен, тогда сигма-тип ∑ a: α, β(a) бесконечен.

LaTeX

$$$\\forall α [Nonempty α]\\ (\\forall a, Infinite (β a))\\ Infinite ((a:α) \\times β a)$$$

Lean4

instance {β : α → Type*} [Nonempty α] [∀ a, Infinite (β a)] : Infinite ((a : α) × β a) :=
  Infinite.sigma_of_right (a := Classical.arbitrary α)

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