eq_zero_of_comapDomain_eq_zero — Mathlib

English

If f is a bijection on l.support, then summing g ∘ f over comapDomain f l equals summing g over l.

Русский

Если f образует биекция на поддержке l, то сумма по g ∘ f от comapDomain f l равна сумме l по g.

LaTeX

$$$$ (\mathrm{comapDomain}\ f\ l\ hf.injOn).sum (g \circ f) = l.sum g. $$$$

Lean4

theorem eq_zero_of_comapDomain_eq_zero [Zero M] (f : α → β) (l : β →₀ M)
    (hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support) : comapDomain f l hf.injOn = 0 → l = 0 :=
  by
  rw [← support_eq_empty, ← support_eq_empty, comapDomain]
  simp_rw [Finset.ext_iff, Finset.notMem_empty, iff_false, mem_preimage]
  intro h a ha
  obtain ⟨b, hb⟩ := hf.2.2 ha
  exact h b (hb.2.symm ▸ ha)

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