finprod_mem_inter_mulSupport_eq' — Mathlib

English

If for all x in mulSupport f we have x∈s ↔ x∈t, then the finprods over s and t coincide.

Русский

Если для каждого x∈mulSupport f выполнено x∈s ⇔ x∈t, тогда финпроизводства по s и по t совпадают.

LaTeX

$$$\\displaystyle (\\forall x, x \\in mulSupport(f) \\rightarrow (x \\in s \\leftrightarrow x \\in t)) \\Rightarrow \\prod\\ᶠ i \\in s, f(i) = \\prod\\ᶠ i \\in t, f(i)$$$

Lean4

@[to_additive]
theorem finprod_mem_inter_mulSupport_eq' (f : α → M) (s t : Set α) (h : ∀ x ∈ mulSupport f, x ∈ s ↔ x ∈ t) :
    ∏ᶠ i ∈ s, f i = ∏ᶠ i ∈ t, f i := by
  apply finprod_mem_inter_mulSupport_eq
  ext x
  exact and_congr_left (h x)

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