English
Let α, β, γ be preordered sets, and s ⊆ α, t ⊆ β. If a is a least element of s and b is a greatest element of t, and f: α × β → γ satisfies that for every b the map a ↦ f(a,b) is antitone, and for every a the map b ↦ f(a,b) is monotone, then f(a,b) is the greatest element of the set { f(x,y) : x ∈ s, y ∈ t }.
Русский
Пусть α, β, γ упорядочены отношениями ≤; пусть s ⊆ α, t ⊆ β. Пусть a является наименьшим элементом s, а b — наибольшим элементом t. Пусть f: α × β → γ удовлетворяет, что для каждого b отображение a ↦ f(a,b) монотонно не возрастает (антитонично), и для каждого a отображение b ↦ f(a,b) монотонно возрастает. Тогда f(a,b) является наибольшим элементом множества { f(x,y) : x ∈ s, y ∈ t }.
LaTeX
$$$ (\\forall b, \\operatorname{Antitone}(\\mathrm{swap}\\ f\\ b)) \\rightarrow (\\forall a, \\operatorname{Monotone}(f\\ a)) \\rightarrow \\IsLeast s\\ a \\rightarrow \\IsGreatest t\\ b \\rightarrow \\IsGreatest(\\mathrm{image2}\\ f\\ s\\ t)\\ (f\\ a\\ b) $$$
Lean4
theorem isGreatest_image2_of_isGreatest (ha : IsLeast s a) (hb : IsGreatest t b) :
IsGreatest (Set.image2 f s t) (f a b) :=
⟨mem_image2_of_mem ha.1 hb.1, mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds h₀ h₁ ha.2 hb.2⟩
