infinite_of_left — Mathlib

English

If α is nontrivial and ι is infinite, then the set of finitely supported functions ι →₀ α is infinite.

Русский

Если α ненулевой и ι бесконечен, то множество конечноподдерживаемых функций ι →₀ α бесконечно.

LaTeX

$$$\\text{Infinite}(ι \\to_0 α)$$$

Lean4

instance infinite_of_left [Nontrivial α] [Infinite ι] : Infinite (ι →₀ α) :=
  let ⟨_, hm⟩ := exists_ne (0 : α)
  Infinite.of_injective _ <| Finsupp.single_left_injective hm

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