infinite_of_exists_right — Mathlib

English

For any i, if π i is infinite, then DFinsupp Π₀ i, π i is infinite.

Русский

Пусть для некоторого i множество π i бесконечное; тогда dfinsupp Π₀ i, π i бесконечен.

LaTeX

$$$\\text{Infinite}(π_i) \\Rightarrow \\text{Infinite}(DFinsupp\\; (π_i))$$$

Lean4

/-- See `DFinsupp.infinite_of_right` for this in instance form, with the drawback that
it needs all `π i` to be infinite. -/
theorem infinite_of_exists_right {ι : Sort _} {π : ι → Sort _} (i : ι) [Infinite (π i)] [∀ i, Zero (π i)] :
    Infinite (Π₀ i, π i) :=
  letI := Classical.decEq ι
  Infinite.of_injective (fun j => DFinsupp.single i j) DFinsupp.single_injective

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