tsum_iSup_eq — Mathlib

English

For any a ∈ α and f : α → ENNReal, ∑' b, ⨆ (a = b) f(b) = f(a).

Русский

Для любой a и функции f выполняется: сумма по b от Sup над условием a=b даёт f(a).

LaTeX

$$$\sum'_{b \in \alpha} \iota_{\{a=b\}} f(b) = f(a)$$$

Lean4

@[simp]
theorem tsum_iSup_eq {α : Type*} (a : α) {f : α → ℝ≥0∞} : (∑' b : α, ⨆ _ : a = b, f b) = f a :=
  (tsum_eq_single a fun _ h => by simp [h.symm]).trans <| by simp

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