English
Restricting the updated vector to a smaller set agrees with updating on the larger set and then restricting.
Русский
Ограничение обновлённого вектора к меньшему множеству согласуется с обновлением по большему множеству и последующим ограничением.
LaTeX
$$$s \\subseteq t \\Rightarrow s.restrict(\\text{updateFinset } x\\ t\\ y) = \\text{restrict}_s\\!\\! _{t} y$$$
Lean4
theorem updateFinset_updateFinset {s t : Finset ι} (hst : Disjoint s t) {y : ∀ i : ↥s, π i} {z : ∀ i : ↥t, π i} :
updateFinset (updateFinset x s y) t z = updateFinset x (s ∪ t) (Equiv.piFinsetUnion π hst ⟨y, z⟩) :=
by
set e := Equiv.Finset.union s t hst
ext i
by_cases his : i ∈ s <;> by_cases hit : i ∈ t <;>
simp only [updateFinset, his, hit, dif_pos, dif_neg, Finset.mem_union, false_or, not_false_iff]
· exfalso; exact Finset.disjoint_left.mp hst his hit
· exact piCongrLeft_sumInl (fun b : ↥(s ∪ t) => π b) e y z ⟨i, his⟩ |>.symm
· exact piCongrLeft_sumInr (fun b : ↥(s ∪ t) => π b) e y z ⟨i, hit⟩ |>.symm
