realize_bdEqual — Mathlib

English

A version of Realize RestrictVarLeft with left-restriction that equates the realizations after applying the inclusion map.

Русский

Версия Realize RestrictVarLeft с левым ограничением, которая эквивалентна реализациям после применения включения.

LaTeX

$$$ (t.restrictVarLeft f).realize (Sum.elim (v ∘ (↑)) xs) = t.realize (Sum.elim v xs) $$$

Lean4

@[simp]
theorem realize_bdEqual (t₁ t₂ : L.Term (α ⊕ (Fin l))) :
    (t₁.bdEqual t₂).Realize v xs ↔ t₁.realize (Sum.elim v xs) = t₂.realize (Sum.elim v xs) :=
  Iff.rfl

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