prod_eq_single — Mathlib

English

There exists a singled-out index a such that under certain nonzero/nonzero conditions, f.prod g reduces to g(a, f(a)).

Русский

Существует выделенный индекс a, такой что при некоторых условиях неравенства элементов поддержке, f.prod g сводится к g(a, f(a)).

LaTeX

$$$$ \\exists a,\\ \\text{conditions} \\Rightarrow f.prod g = g(a, f(a)) $$$$

Lean4

@[to_additive]
theorem prod_eq_single {f : α →₀ M} (a : α) {g : α → M → N} (h₀ : ∀ b, f b ≠ 0 → b ≠ a → g b (f b) = 1)
    (h₁ : f a = 0 → g a 0 = 1) : f.prod g = g a (f a) :=
  by
  refine Finset.prod_eq_single a (fun b hb₁ hb₂ => ?_) (fun h => ?_)
  · exact h₀ b (mem_support_iff.mp hb₁) hb₂
  · simp only [notMem_support_iff] at h
    rw [h]
    exact h₁ h

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