listProd — Mathlib

English

If each f_i is equivalent to g_i along l for i in a list L, then the product over i in L of f_i is equivalent to the product of g_i along l.

Русский

Если для каждого i в списке L f_i эквивалентно g_i по l, то произведение ∏ f_i эквивалентно ∏ g_i по l.

LaTeX

$$$ \\forall i \\in L,\\ f_i \\sim_{l} g_i \\Rightarrow \\big( \\prod_{i \\in L} f_i(\\cdot) \\big) \\sim_{l} \\big( \\prod_{i \\in L} g_i(\\cdot) \\big) $$$

Lean4

theorem listProd {L : List ι} {f g : ι → α → β} (h : ∀ i ∈ L, f i ~[l] g i) :
    (fun x ↦ (L.map (f · x)).prod) ~[l] (fun x ↦ (L.map (g · x)).prod) := by
  induction L with
  | nil => simp [IsEquivalent.refl]
  | cons i L ihL =>
    simp only [List.forall_mem_cons, List.map_cons, List.prod_cons] at h ⊢
    exact h.1.mul (ihL h.2)

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