English
For sets s ⊆ α and t ⊆ β that are finite, the toFinset of image2 f s t matches the Finset image₂ of the toFinset representations of s and t.
Русский
Пусть s ⊆ α и t ⊆ β конечны. Тогда toFinset от image2 f s t совпадает с Finset.image₂ от toFinset(s) и toFinset(t).
LaTeX
$$$(\\operatorname{image}_2 f\, s\, t)^{\\mathrm{toFinset}} = \\operatorname{Finset.image}_2 f\, s^{\\mathrm{toFinset}} t^{\\mathrm{toFinset}}$$$
Lean4
@[simp]
theorem toFinset_image2 (f : α → β → γ) (s : Set α) (t : Set β) [Fintype s] [Fintype t] [Fintype (image2 f s t)] :
(image2 f s t).toFinset = Finset.image₂ f s.toFinset t.toFinset :=
Finset.coe_injective <| by simp
