realize_mem — Mathlib

English

If every variable maps into S, then the interpretation of any term t under xs lies in S.

Русский

Если каждая переменная отображается в S, то интерпретация любой термы t по xs лежит в S.

LaTeX

$$$$ \forall t,\; xs,\; (\forall a, xs(a) \in S) \Rightarrow t.realize(xs) \in S $$$$

Lean4

theorem realize_mem {α : Type*} (t : L.Term α) (xs : α → M) (h : ∀ a, xs a ∈ S) : t.realize xs ∈ S := by
  induction t with
  | var a => exact h a
  | func f ts ih => exact Substructure.fun_mem _ _ _ ih

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