updateFinset_updateFinset_of_subset

English

Restricting the updated vector to a subset equals restricting the function y to that subset after updating.

Русский

Ограничение обновлённого вектора к подмножеству равно ограничению функции y до этого подмножества после обновления.

LaTeX

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

Lean4

theorem updateFinset_updateFinset_of_subset {s t : Finset ι} (hst : s ⊆ t) (x : Π i, π i) (y : Π i : s, π i)
    (z : Π i : t, π i) : updateFinset (updateFinset x s y) t z = updateFinset x t z :=
  by
  ext i
  simp only [updateFinset]
  split_ifs with h1 h2 <;> try rfl
  exact (h1 (hst h2)).elim

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