boundedFormula — Mathlib

English

A relation can be applied to a finite collection of terms to form a bounded formula; this formalizes the idea of a predicate over a bounded tuple of terms.

Русский

К relation может быть применена к конечной совокупности термов, образуя ограниченную формулу; это задаёт предикат над ограниченной кортежем термов.

LaTeX

$$$R:\\;L.Relations(n),\\ ts: Fin\\ n \\to L.Term(\\alpha \\oplus (Fin\\ l))\\ \\Rightarrow \\; L.BoundedFormula(\\alpha,l)$ with $R.boundedFormula(ts)$$$

Lean4

/-- Applies a relation to terms as a bounded formula. -/
def boundedFormula {l : ℕ} (R : L.Relations n) (ts : Fin n → L.Term (α ⊕ (Fin l))) : L.BoundedFormula α l :=
  BoundedFormula.rel R ts

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