realize_restrictVar' — Mathlib

English

A special simplified case of restrictVar: restricting by an inclusion of a subset preserves realization up to composing v with the inclusion map.

Русский

Упрощённый частный случай restrictVar: ограничение на подмножество сохраняет реализацию через композицию с включением.

LaTeX

$$$ (t.restrictVar (Set.inclusion h)).realize (v \circ (\uparrow)) = t.realize v $$$

Lean4

/-- A special case of `realize_restrictVar`, included because we can add the `simp` attribute
to it -/
@[simp]
theorem realize_restrictVar' [DecidableEq α] {t : L.Term α} {s : Set α} (h : ↑t.varFinset ⊆ s) {v : α → M} :
    (t.restrictVar (Set.inclusion h)).realize (v ∘ (↑)) = t.realize v :=
  realize_restrictVar _ (by simp)

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