English
Let s ⊆ α and t ⊆ β be bounded, and suppose that for every b ∈ t the map a ↦ f(a,b) is K1-Lipschitz on s, and for every a ∈ s the map b ↦ f(a,b) is K2-Lipschitz on t. Then the two-variable image set { f(a,b) : a ∈ s, b ∈ t } is bounded.
Русский
Пусть s ⊆ α и t ⊆ β ограничены, и пусть для каждого b ∈ t отображение a ↦ f(a,b) является K1‑липшицевым на s, а для каждого a ∈ s отображение b ↦ f(a,b) является K2‑липшицевым на t. Тогда множество { f(a,b) : a ∈ s, b ∈ t } ограничено.
LaTeX
$$$ (\\operatorname{IsBounded}(s) \\\\land \\operatorname{IsBounded}(t) \\\\land \\forall b \\in t,\\; \\operatorname{LipschitzOnWith}(K_1, (\\lambda a, f(a,b)), s) \\\\land \\forall a \\in s,\\; \\operatorname{LipschitzOnWith}(K_2, f(a), t)) \\Rightarrow \\operatorname{IsBounded}(\\{ f(a,b) \\mid a \\in s, b \\in t \\}). $$$
Lean4
theorem isBounded_image2 (f : α → β → γ) {K₁ K₂ : ℝ≥0} {s : Set α} {t : Set β} (hs : Bornology.IsBounded s)
(ht : Bornology.IsBounded t) (hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun a => f a b) s)
(hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t) : Bornology.IsBounded (Set.image2 f s t) :=
Metric.isBounded_iff_ediam_ne_top.2 <|
ne_top_of_le_ne_top
(ENNReal.add_ne_top.mpr
⟨ENNReal.mul_ne_top ENNReal.coe_ne_top hs.ediam_ne_top, ENNReal.mul_ne_top ENNReal.coe_ne_top ht.ediam_ne_top⟩)
(ediam_image2_le _ _ _ hf₁ hf₂)
