English
If a Finset u is a subset of the image of two sets s and t under a binary operation f, then there exist Finsets s' ⊆ s and t' ⊆ t with u ⊆ image₂ f s' t'.
Русский
Если Finset u ⊆ image₂ f s t, то найдутся Finsets s' ⊆ s, t' ⊆ t такие, что u ⊆ image₂ f s' t'.
LaTeX
$$$\\forall s:\\ Set\\,\\alpha, \\forall t:\\ Set\\,\\beta, (u \\subseteq image2 f s t) \\Rightarrow \\exists s'\\subseteq s, \\exists t'\\subseteq t, u \\subseteq image_2 f s' t'$$$
Lean4
/-- If a `Finset` is a subset of the image of two `Set`s under a binary operation,
then it is a subset of the `Finset.image₂` of two `Finset` subsets of these `Set`s. -/
theorem subset_set_image₂ {s : Set α} {t : Set β} (hu : ↑u ⊆ image2 f s t) :
∃ (s' : Finset α) (t' : Finset β), ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ image₂ f s' t' :=
by
rw [← Set.image_prod, subset_set_image_iff] at hu
rcases hu with ⟨u, hu, rfl⟩
classical
use u.image Prod.fst, u.image Prod.snd
simp only [coe_image, Set.image_subset_iff, image₂_image_left, image₂_image_right, image_subset_iff]
exact ⟨fun _ h ↦ (hu h).1, fun _ h ↦ (hu h).2, fun x hx ↦ mem_image₂_of_mem hx hx⟩
