English
For a family of types indexed by ι with finite index set, the piFinset of image₂s equals the image₂ of the pointwise images: piFinset_i image₂ (f_i) (s_i) (t_i) = image₂ (f_i) over piFinset s and piFinset t.
Русский
Для семейства типов, индексированного множеством ι, с конечным индексным набором, пирефинсет изображения₂ совпадает с изображением₂ по поканальным образам: piFinset image₂ = image₂ на piFinset.
LaTeX
$$$\pi\mathrm{Finset}\,\big(\lambda i.\operatorname{image}_2 (f i) (s i) (t i)\big) = \operatorname{image}_2 \big(\lambda a b i. f i (a i) (b i)\big) (\pi\mathrm{Finset} s) (\pi\mathrm{Finset} t)$$$
Lean4
theorem piFinset_image₂ (f : ∀ i, α i → β i → γ i) (s : ∀ i, Finset (α i)) (t : ∀ i, Finset (β i)) :
piFinset (fun i ↦ image₂ (f i) (s i) (t i)) = image₂ (fun a b i ↦ f _ (a i) (b i)) (piFinset s) (piFinset t) := by
ext; simp only [mem_piFinset, mem_image₂, Classical.skolem, forall_and, funext_iff]
