English
If s and t are subsingleton sets, then image2 f s t is a subsingleton as well.
Русский
Если s и t являются подсемействами (subsingleton), то image2 f s t тоже подсемейство.
LaTeX
$$$$\\text{If } s\\text{ and } t\\text{ are subsingleton, then } image2\\ f\\ s\\ t\\text{ is subsingleton.} $$$$
Lean4
theorem image2 (hs : s.Subsingleton) (ht : t.Subsingleton) (f : α → β → γ) : (image2 f s t).Subsingleton :=
by
rw [← image_prod]
apply (hs.prod ht).image