realize_term_substructure — Mathlib

English

For a substructure S of M and a term t with arguments in S, the interpretation of t under the inclusion equals the interpretation of t in M.

Русский

Для подпредставления S под M и терма t с аргументами в S, смысловое значение t под вставлением совпадает с смысловым значением t в M.

LaTeX

$$$t^{S}(v) = \iota\left(t^{M}(v)\right)$, where $\iota: S \hookrightarrow M$ is the inclusion$$

Lean4

@[simp]
theorem realize_term_substructure {α : Type*} {S : L.Substructure M} (v : α → S) (t : L.Term α) :
    t.realize ((↑) ∘ v) = (↑(t.realize v) : M) :=
  HomClass.realize_term S.subtype

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