map_fun — Mathlib

English

For φ: M →[L] N and a function symbol f of arity n, applying φ to the evaluation of f on x is the same as evaluating f on φ∘x.

Русский

Для φ: M →[L] N и символьной функции f арности n, применение φ к значению f над x равно значению f над φ∘x.

LaTeX

$$$\\phi\\,(\\mathrm{funMap}\\ f\\ x) = \\mathrm{funMap}\\ f\\ (\\phi\\circ x)$$$

Lean4

@[simp]
theorem map_fun (φ : M →[L] N) {n : ℕ} (f : L.Functions n) (x : Fin n → M) : φ (funMap f x) = funMap f (φ ∘ x) :=
  HomClass.map_fun φ f x

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