comp_fin3 — Mathlib

English

For any functions f: R → S and a triple (a, b, c) ∈ R^3, the equality f ∘ ![a,b,c] = ![f a, f b, f c] holds, i.e. composition with f is applied componentwise.

Русский

Для функции f: R → S и тройки (a,b,c) ∈ R^3 выполняется равенство f ∘ ![a,b,c] = ![f a, f b, f c], то есть композиция с f действует по компонентам.

LaTeX

$$$f \circ ![a,b,c] = ![f a, f b, f c]$$$

Lean4

theorem comp_fin3 (f : R → S) (a b c : R) : f ∘ ![a, b, c] = ![f a, f b, f c] :=
  (FinVec.map_eq ..).symm

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