English
Let ha be IsGreatest s a and hb be IsLeast t b. If for all b the map a ↦ f(a,b) is antitone and for all a the map b ↦ f(a,b) is monotone, then f(a,b) is the least element of { f(x,y) : x ∈ s, y ∈ t }.
Русский
Пусть ha = IsGreatest s a, hb = IsLeast t b. Пусть f: α × β → γ удовлетворяет тем же условиям антитоничности/монотонности. Тогда 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 \\IsGreatest s a \\rightarrow \\IsLeast t b \\rightarrow \\IsLeast(\\mathrm{image2}\\ f\\ s\\ t)\\ (f\\ a\\ b) $$$
Lean4
theorem isLeast_image2_of_isLeast (ha : IsGreatest s a) (hb : IsLeast t b) : IsLeast (Set.image2 f s t) (f a b) :=
⟨mem_image2_of_mem ha.1 hb.1, mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds h₀ h₁ ha.2 hb.2⟩
