formula — Mathlib

English

Applies a relation R to a tuple of term interpretations to form a formula.

Русский

Применяет отношение R к кортежу трактовок термов, образуя формулу.

LaTeX

$$$\\text{formula}(R, ts) := R.\\text{boundedFormula}(\\lambda i. (ts(i)).\\text{relabel Sum.inl})$$$

Lean4

/-- Applies a relation to terms as a formula. -/
def formula (R : L.Relations n) (ts : Fin n → L.Term α) : L.Formula α :=
  R.boundedFormula fun i => (ts i).relabel Sum.inl

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