map_fun — Mathlib

English

Let φ: M ≃[L] N and f be an n-ary function symbol. Then φ preserves the interpretation of f: φ(f^M(x)) = f^N(φ∘x) for x: Fin n → M.

Русский

Пусть φ: M ≃_L N и f — символ функции ранга n. Тогда φ сохраняет интерпретацию f: φ(f^M(x)) = f^N(φ(x_1),…,φ(x_n)) для x: Fin n → M.

LaTeX

$$$\forall n, \phi\bigl(f^M(x)\bigr) = f^N\bigl(\phi\circ x\bigr)$$$

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

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