map₂_map_left — Mathlib

English

Applying map₂ with a function f₁ after mapping f₂ on the first vector equals applying a composed map₂ with f₁ ∘ f₂ on the two vectors.

Русский

Применение map₂ с функцией f₁ после отображения f₂ на первую компоненту эквивалентно отображению через составную функцию f₁ ∘ f₂ на два вектора.

LaTeX

$$$\text{map}_2 f_1 (\text{map } f_2 \ xs) = \text{map}_2 (\lambda x y. f_1 (f_2 x) y) xs ys$$$

Lean4

@[simp]
theorem map₂_map_left (f₁ : γ → β → ζ) (f₂ : α → γ) : map₂ f₁ (map f₂ xs) ys = map₂ (fun x y => f₁ (f₂ x) y) xs ys := by
  induction xs, ys using Vector.revInductionOn₂ <;> simp_all

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