product — Mathlib

English

If l1 ~ l2 and t1 ~ t2, then l1.product t1 ~ l2.product t2.

Русский

Если l1 перестановочно эквивалентен l2 и t1 перестановочно эквивалентен t2, то их произведения перестановочно эквивалентны.

LaTeX

$$$l_1 \\sim l_2 \\land t_1 \\sim t_2 \\Rightarrow (l_1 \\mathrm{.product} \\; t_1) \\sim (l_2 \\mathrm{.product} \\; t_2)$$$

Lean4

@[gcongr]
theorem product {l₁ l₂ : List α} {t₁ t₂ : List β} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) : product l₁ t₁ ~ product l₂ t₂ :=
  (p₁.product_right t₁).trans (p₂.product_left l₂)

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