English
Updating a coordinate by a larger finite set corresponds to restricting to those functions whose i-th coordinate lies in the new set.
Русский
Обновление i-й координаты более крупным конечным множеством эквивалентно ограничению функций теми значениями i-й координаты, которые лежат в новом множестве.
LaTeX
$$$\\operatorname{piFinset}(\\lambda j. s_j)_{\text{update } i t} = \\{ f \\in \\operatorname{piFinset}(\\lambda j. s_j) \\mid f(i) \\in t \\}.$$$
Lean4
theorem piFinset_update_eq_filter_piFinset_mem (s : ∀ i, Finset (δ i)) (i : α) {t : Finset (δ i)} (hts : t ⊆ s i) :
piFinset (Function.update s i t) = {f ∈ piFinset s | f i ∈ t} :=
by
ext f
simp only [mem_piFinset, mem_filter]
refine ⟨fun h ↦ ?_, fun h j ↦ ?_⟩
· have := by simpa using h i
refine ⟨fun j ↦ ?_, this⟩
obtain rfl | hji := eq_or_ne j i
· exact hts this
· simpa [hji] using h j
· obtain rfl | hji := eq_or_ne j i
· simpa using h.2
· simpa [hji] using h.1 j
