English
Let x be a family of elements indexed by ι and s a finite subset of ι. Then updating x on s using the restriction of x to s yields x.
Русский
Пусть x представляет семейство элементов, индексируемых по ι, и s является конечным подмножеством ι. Тогда восстановление x на s с помощью ограниченного значения x на s дает исходную функцию.
LaTeX
$$$\\operatorname{updateFinset}(x, s, s\\restriction x) = x$$$
Lean4
@[simp]
theorem updateFinset_restrict {s : Finset ι} (x : Π i, π i) : updateFinset x s (s.restrict x) = x :=
by
ext i
simp [updateFinset]