bdEqual — Mathlib

English

The equality of two terms is expressed as a bounded formula using the equality predicate of the bounded formula framework.

Русский

Равенство двух термов выражается как ограниченная формула с использованием предиката равенства в рамках ограниченной формулы.

LaTeX

$$$\\mathrm{bdEqual}(t_1,t_2) = \\mathrm{BoundedFormula}.equal(t_1,t_2)$$$

Lean4

/-- The equality of two terms as a bounded formula. -/
def bdEqual (t₁ t₂ : L.Term (α ⊕ (Fin n))) : L.BoundedFormula α n :=
  BoundedFormula.equal t₁ t₂

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