map_fun — Mathlib

English

Reiterated formulation of Equiv_iSup application at i.

Русский

Повторное применение Equiv_iSup на узле i.

LaTeX

$$$\\mathrm{Equiv\_iSup} S\\bigl(\\mathrm{of}_{L\\iota G f i} x\\bigr) = \\mathrm{Substructure.inclusion}(\\mathrm{le\_iSup}\\ _\\ _) x.$$$

Lean4

@[simp]
theorem map_fun (φ : M ↪ₑ[L] N) {n : ℕ} (f : L.Functions n) (x : Fin n → M) : φ (funMap f x) = funMap f (φ ∘ x) :=
  by
  have h := φ.map_formula (Formula.graph f) (Fin.cons (funMap f x) x)
  rw [Formula.realize_graph, Fin.comp_cons, Formula.realize_graph] at h
  rw [eq_comm, h]

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