tprod_one — Mathlib

English

If for all b, f(b) equals 1 outside a finite set s, then tprod equals the finite product over s.

Русский

Если вне конечного множества s f(b)=1, то tprod равен произведению по s.

LaTeX

$$Eq (tprod (fun b => f b) L) (s.prod fun b => f b)$$

Lean4

@[to_additive (attr := simp)]
theorem tprod_one : ∏'[L] _, (1 : α) = 1 := by
  rw [tprod_def, dif_pos multipliable_one, mulSupport_fun_one, Set.empty_inter, Set.mulIndicator_one, finprod_one,
    eq_true_intro hasProd_one, if_true, ite_self]

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