infinite_of_left — Mathlib

English

If ι is infinite and every π i is nontrivial with a zero, then DFinsupp Π₀ i, π i is infinite.

Русский

Если ι бесконечен и каждый π i непустой полем, то DFinsupp Π₀ i, π i бесконечен.

LaTeX

$$$\\text{Infinite}(DFinsupp\\; (\\lambda i. π i))$$$

Lean4

instance infinite_of_left {ι : Sort _} {π : ι → Sort _} [∀ i, Nontrivial (π i)] [∀ i, Zero (π i)] [Infinite ι] :
    Infinite (Π₀ i, π i) := by
  letI := Classical.decEq ι; choose m hm using fun i => exists_ne (0 : π i)
  exact Infinite.of_injective _ (DFinsupp.single_left_injective hm)

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