wInner_of_isEmpty — Mathlib

English

If the index set is empty, the weighted inner product is zero for all f and g.

Русский

Если множество индексов пусто, взвешенное скалярное произведение равно нулю для любых f и g.

LaTeX

$$$\ll f, g \gg_{\mathbb{K}, w} = 0$ при IsEmpty ι$$

Lean4

@[simp]
theorem wInner_of_isEmpty [IsEmpty ι] (w : ι → ℝ) (f g : ∀ i, E i) : ⟪f, g⟫_[𝕜, w] = 0 := by
  simp [Subsingleton.elim f 0]

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