realize_equal — Mathlib

English

The realization of equality between two terms is equivalent to the equality of their realizations.

Русский

Реализация равенства двух термов эквивалентна равенству их реализаций.

LaTeX

$$$ (t_1 = t_2)^M(x) \iff t_1^M(x) = t_2^M(x) $$$

Lean4

@[simp]
theorem realize_equal {t₁ t₂ : L.Term α} {x : α → M} : (t₁.equal t₂).Realize x ↔ t₁.realize x = t₂.realize x := by
  simp [Term.equal, Realize]

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