English
If a is a greatest element of s and b is a greatest element of t, then f(a, b) is a greatest element of image2 f s t.
Русский
Если a — наибольший элемент множества s, а b — наибольший элемент множества t, тогда f(a, b) — наибольший элемент множества image2 f s t.
LaTeX
$$$\\big( IsGreatest\\, s\\, a \\big) \\to \\big( IsGreatest\\, t\\, b \\big) \\to IsGreatest(\\operatorname{image2} f\\, s\\, t,\\ f a b)$$$
Lean4
protected theorem image2 (ha : IsGreatest s a) (hb : IsGreatest t b) : IsGreatest (image2 f s t) (f a b) :=
⟨mem_image2_of_mem ha.1 hb.1, mem_upperBounds_image2 h₀ h₁ ha.2 hb.2⟩