linearCombination_comapDomain — Mathlib

English

For f : α → α', l : α' →₀ R and hf: InjOn f (f⁻¹' ↑l.supp), the linearCombination R v applied to comapDomain f l hf equals the sum over i in l.support.preimage f hf of l (f i) • v i.

Русский

Для f: α → α', l: α' →₀ R и hf: InjOn f ..., линейная комбинация над v, применённая к comapDomain f l hf, равна сумме по i из preimage l, l (f i) • v i.

LaTeX

$$$\\operatorname{linearCombination}_R v (\\mathrm{Finsupp.comapDomain} f\, l\, hf) = (l.\\text{support}.preimage f hf).sum \\bigl(\\lambda i. l (f i) \\;\\cdot\\; v i\\bigr)$$$

Lean4

theorem linearCombination_comapDomain (f : α → α') (l : α' →₀ R) (hf : Set.InjOn f (f ⁻¹' ↑l.support)) :
    linearCombination R v (Finsupp.comapDomain f l hf) = (l.support.preimage f hf).sum fun i => l (f i) • v i := by
  rw [linearCombination_apply]; rfl

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