restrict_updateFinset_of_subset — Mathlib

English

If s ⊆ t, restricting the updated vector to s equals restricting y to s.

Русский

Если s ⊆ t, ограничение обновления до s эквивалентно ограничению y до s.

LaTeX

$$$s \\subseteq t \\Rightarrow s.restrict(\\text{updateFinset } x t y) = \\text{restrict}_s y$$$

Lean4

theorem restrict_updateFinset_of_subset {s t : Finset ι} (hst : s ⊆ t) (x : Π i, π i) (y : Π i : t, π i) :
    s.restrict (updateFinset x t y) = restrict₂ hst y := by
  ext i
  simp [updateFinset, dif_pos (hst i.2)]

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