hsum_unique — Mathlib

English

If the index type is unique, the hsum of a family equals the chosen default element.

Русский

Если множество индексов уникально, сумма по Хану равна заданному значению по умолчанию.

LaTeX

$$$\\forall ι\\ [Unique ι],\\ (x : HahnSeries.SummableFamily Γ R ι)\\; x.hsum = x default$$$

Lean4

@[simp]
theorem hsum_unique {ι} [Unique ι] (x : SummableFamily Γ R ι) : x.hsum = x default :=
  by
  ext g
  simp only [coeff_hsum, finsum_unique]

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