realize_constants — Mathlib

English

Let c be a constant in the language L. For any M and any valuation v : α → M, the interpretation of the constant c, viewed as a term, is exactly the element c itself in M.

Русский

Пусть c — константа языка L. Для любой M и любой оценивания v : α → M, интерпретация константы c (как терма) равна самому элементу c в M.

LaTeX

$$$ c.term.realize\, v = c $$$

Lean4

@[simp]
theorem realize_constants {c : L.Constants} {v : α → M} : c.term.realize v = c :=
  funMap_eq_coe_constants

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