map_onFunction — Mathlib

English

If f is a function in L and ϕ is an expansion, then funMap(ϕ.onFunction f) = funMap f.

Русский

Если f — функция в языке L, и ϕ — расширение, то funMap(ϕ.onFunction f) = funMap f.

LaTeX

$$$\mathrm{funMap}(\varphi.onFunction f)\; x = \mathrm{funMap} f\; x$ for all x$$

Lean4

@[simp]
theorem map_onFunction {M : Type*} [L.Structure M] [L'.Structure M] [ϕ.IsExpansionOn M] {n} (f : L.Functions n)
    (x : Fin n → M) : funMap (ϕ.onFunction f) x = funMap f x :=
  IsExpansionOn.map_onFunction f x

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