realize_lt — Mathlib

English

If t1.lt t2 holds in the realized terms, then the underlying order satisfies t1 < t2.

Русский

Если t1.lt t2 истинно для реализованных термов, то в исходном порядке выполняется t1 < t2.

LaTeX

$$$ (t_{1}.lt t_{2}).Realize\; v\\ xs \\\\iff t_{1}.realize (Sum.elim\, v\, xs) < t_{2}.realize (Sum.elim\, v\, xs) $$$

Lean4

@[simp]
theorem realize_lt {t₁ t₂ : L.Term (α ⊕ (Fin n))} {v : α → M} {xs : Fin n → M} :
    (t₁.lt t₂).Realize v xs ↔ t₁.realize (Sum.elim v xs) < t₂.realize (Sum.elim v xs) := by
  simp [Term.lt, lt_iff_le_not_ge]

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