formula₂ — Mathlib

English

A binary relation applied to two terms yields a formula by relabeling their arguments appropriately.

Русский

Двоичное отношение, применённое к двум термам, образует формулу, выполнив переназначение аргументов.

LaTeX

$$$\\text{formula}_2(R,t_1,t_2) = R.formula([t_1,t_2])$$$

Lean4

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

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