sum_finsupport' — Mathlib

English

For each x0, the set {i | x0 ∈ tsupport(f_i)} is finite.

Русский

Для каждой x0 множество индексов {i | x0 ∈ tsupport(f_i)} конечно.

LaTeX

$$$\{ i \mid x_0 \in tsupport(ρ i)\}.\text{Finite}$$$

Lean4

theorem sum_finsupport' (hx₀ : x₀ ∈ s) {I : Finset ι} (hI : ρ.finsupport x₀ ⊆ I) : ∑ i ∈ I, ρ i x₀ = 1 := by
  classical
  rw [← Finset.sum_sdiff hI, ρ.sum_finsupport hx₀]
  suffices ∑ i ∈ I \ ρ.finsupport x₀, (ρ i) x₀ = ∑ i ∈ I \ ρ.finsupport x₀, 0 by
    rw [this, add_eq_right, Finset.sum_const_zero]
  apply Finset.sum_congr rfl
  rintro x hx
  simp only [Finset.mem_sdiff, ρ.mem_finsupport, mem_support, Classical.not_not] at hx
  exact hx.2

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