sum_extend_zero — Mathlib

English

If f is an injective function, extending the index by 0 does not change the total sum: sum (extend f m 0) = sum m.

Русский

Если f инъективна, расширение индекса нулём не меняет общую сумму: sum (extend f m 0) = sum m.

LaTeX

$$$ \text{sum}(\text{Function.extend } f\; m\; 0) = \text{sum } m $$$

Lean4

@[simp]
theorem sum_extend_zero {ι ι' : Type*} {f : ι → ι'} (hf : Injective f) (m : ι → Measure α) :
    sum (Function.extend f m 0) = sum m := by
  ext s hs
  simp [*, Function.apply_extend (fun μ : Measure α ↦ μ s)]

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