English
The image of a binary function f: α → β → γ as a Set function is the set of all outputs f(a,b) with a ∈ s and b ∈ t.
Русский
Образ бинарной функции f: α → β → γ на множествах s и t — множество всех значений f(a,b) с a ∈ s, b ∈ t.
LaTeX
$$$$ \\operatorname{image2}(f,s,t) = \\{ c \\mid \\exists a \\in s, \\exists b \\in t, f(a,b) = c \\} $$$$
Lean4
/-- The image of a binary function `f : α → β → γ` as a function `Set α → Set β → Set γ`.
Mathematically this should be thought of as the image of the corresponding function `α × β → γ`. -/
def image2 (f : α → β → γ) (s : Set α) (t : Set β) : Set γ :=
{c | ∃ a ∈ s, ∃ b ∈ t, f a b = c}
