listProd — Mathlib

English

If two lists of elements are pairwise joined, then the product of the lists is joined.

Русский

Если два списка элементов попарно связаны путём, то их суммарный продукт связан.

LaTeX

$$$List.Forall₂ Joined l l' \Rightarrow Joined l.prod l'.prod$$$

Lean4

@[to_additive]
theorem listProd {M : Type*} [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] {l l' : List M}
    (h : List.Forall₂ Joined l l') : Joined l.prod l'.prod := by
  induction h with
  | nil => rfl
  | cons h₁ _ h₂ => exact h₁.mul h₂

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