realize_rel — Mathlib

English

The realization of a bounded formula with a relation symbol R corresponds to the relation map of R evaluated on the realizations of the terms.

Русский

Реализация ограниченной формулы с отношением R соответствует отображению отношения R на реализациях терминов.

LaTeX

$$$ (R.formula ts).Realize v \iff RelMap R (\lambda i. (ts i).realize v) $$$

Lean4

@[simp]
theorem realize_rel {k : ℕ} {R : L.Relations k} {ts : Fin k → L.Term α} :
    (R.formula ts).Realize v ↔ RelMap R fun i => (ts i).realize v :=
  BoundedFormula.realize_rel.trans (by simp)

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