finite_support — Mathlib

English

For any finitely supported function f, the set of indices where f(i) ≠ 0 is finite.

Русский

Для любой конечноподдерживаемой функции f множество индексов, на которых f(i) ≠ 0, конечна.

LaTeX

$$$\{ i \mid f(i) \neq 0 \}$ is finite$$

Lean4

theorem finite_support (f : Π₀ i, β i) : Set.Finite {i | f i ≠ 0} :=
  Trunc.induction_on f.support' fun xs ↦ xs.1.finite_toSet.subset fun i H ↦ ((xs.prop i).resolve_right H)

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