English
If s has least element a and t has least element b, then Set.image2 f s t has a greatest element f(a,b), under suitable monotonicity assumptions.
Русский
Если у множеств s и t есть наименьшие элементы a и b соответственно, то изображение image2 f s t имеет наибольший элемент f(a,b) при подходящих предположениях монотонности.
LaTeX
$$∀ {α β γ} [Preorder α] [Preorder β] [Preorder γ] {f : α → β → γ} {s : Set α} {t : Set β} {a : α} {b : β},
(∀ (b : β), Antitone (Function.swap f b)) →
(∀ (a : α), Antitone (f a)) → IsLeast s a → IsLeast t b → IsGreatest (Set.image2 f s t) (f a b)$$
Lean4
theorem isGreatest_image2 (ha : IsLeast s a) (hb : IsLeast t b) : IsGreatest (Set.image2 f s t) (f a b) :=
⟨mem_image2_of_mem ha.1 hb.1, mem_upperBounds_image2_of_mem_lowerBounds h₀ h₁ ha.2 hb.2⟩
