weightedVSub_empty — Mathlib

English

The weightedVSub over an empty index set is the zero vector, regardless of the weights and the target map.

Русский

В взвешенной сумме над пустым набором индексов получается нулевой вектор, независимо от весов и целевой отображения.

LaTeX

$$$\displaystyle (\varnothing : \mathrm{Finset}\; \iota).weightedVSub p w = 0$$$

Lean4

/-- The `weightedVSub` for an empty set is 0. -/
@[simp]
theorem weightedVSub_empty (w : ι → k) (p : ι → P) : (∅ : Finset ι).weightedVSub p w = (0 : V) := by
  simp [weightedVSub_apply]

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