English
Symmetric to the previous result: if all slices a ↦ f(a,b) are AntilipschitzWith K₂, then boundedness of image2 f s t implies boundedness of s or t.
Русский
Обобщение слева на правую сторону: если все срезы f(a,·) удовлетворяют антилипшицевости, то ограниченность image2 f s t влечёт ограниченность хотя бы одного из s, t.
LaTeX
$$$ \forall a, \operatorname{AntilipschitzWith} K_2 (\lambda b, f(a,b)) \Rightarrow \left( \operatorname{IsBounded}(\operatorname{image2} f s t) \rightarrow (\operatorname{IsBounded}(s) \lor \operatorname{IsBounded}(t)) \right)$$$
Lean4
theorem isBounded_of_image2_right {f : α → β → γ} {K₂ : ℝ≥0} (hf : ∀ a, AntilipschitzWith K₂ (f a)) {s : Set α}
{t : Set β} (hst : IsBounded (Set.image2 f s t)) : IsBounded s ∨ IsBounded t :=
Or.symm <| isBounded_of_image2_left (flip f) hf <| image2_swap f s t ▸ hst
