instSigmaOfNonempty — Mathlib

English

If α is infinite and each fiber β(a) is nonempty, then the dependent sum Σ a: α, β(a) is infinite.

Русский

Если α бесконечен, а для каждого a не пусто β(a), то сумма по зависимости ∑_{a∈α} β(a) бесконечна.

LaTeX

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

Lean4

instance {β : α → Type*} [Infinite α] [∀ a, Nonempty (β a)] : Infinite ((a : α) × β a) :=
  Infinite.of_surjective Sigma.fst Sigma.fst_surjective

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