sum_comapDomain — Mathlib

English

If f is injective, then mapDomain f is injective.

Русский

Если f инъективен, то mapDomain f инъективен.

LaTeX

$$$$ \mathrm{Function.Injective}(\mathrm{mapDomain}\ f). $$$$

Lean4

theorem sum_comapDomain [Zero M] [AddCommMonoid N] (f : α → β) (l : β →₀ M) (g : β → M → N)
    (hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support) : (comapDomain f l hf.injOn).sum (g ∘ f) = l.sum g :=
  Finset.sum_preimage_of_bij f _ hf fun x => g x (l x)

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