boundedFormula₁ — Mathlib

English

A 2-ary relation applied to two terms yields a bounded formula of the appropriate arity.

Русский

Двухарная отношение, применённое к двум термам, образует ограниченную формулу нужной арности.

LaTeX

$$$R\\in L.Relations(2),\\ t_1,t_2\\in L.Term(\\alpha)\\ \\Rightarrow \\; R.boundedFormula([t_1,t_2]) \\in L.BoundedFormula(\\alpha,\\, ?)$$$

Lean4

/-- Applies a unary relation to a term as a bounded formula. -/
def boundedFormula₁ (r : L.Relations 1) (t : L.Term (α ⊕ (Fin n))) : L.BoundedFormula α n :=
  r.boundedFormula ![t]

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