infinite_of_right — Mathlib

English

Let ι be a nonempty type and each π i be an infinite type with a zero. Then the dependent finitely supported product DFinsupp (Π₀ i, π i) is infinite.

Русский

Пусть ι — непустой тип и для каждого i ∈ ι дано бесконечное множество π i с нулём. Тогда зависимое множество DFinsupp (Π₀ i, π i) бесконечно.

LaTeX

$$$|\Pi_0 i, \pi i| = \infty$$$

Lean4

/-- See `DFinsupp.infinite_of_exists_right` for the case that only one `π ι` is infinite. -/
instance infinite_of_right {ι : Sort _} {π : ι → Sort _} [∀ i, Infinite (π i)] [∀ i, Zero (π i)] [Nonempty ι] :
    Infinite (Π₀ i, π i) :=
  DFinsupp.infinite_of_exists_right (Classical.arbitrary ι)

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