boundedFormula₂ — Mathlib

English

A binary relation can be interpreted as a formula by applying it to two terms after relabelling their variables appropriately.

Русский

Двоичное отношение может быть интерпретировано как формула через применение к двум термам с соответствующим переназначением переменных.

LaTeX

$$$R.formula([t_1,t_2]) = R.boundedFormula([t_1,t_2])$$$

Lean4

/-- Applies a binary relation to two terms as a bounded formula. -/
def boundedFormula₂ (r : L.Relations 2) (t₁ t₂ : L.Term (α ⊕ (Fin n))) : L.BoundedFormula α n :=
  r.boundedFormula ![t₁, t₂]

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