English
If, for every b ∈ t, the map a ↦ f a b is LipschitzOnWith K1 on s, and for every a ∈ s the map b ↦ f a b is LipschitzOnWith K2 on t, then the diameter of image2 f s t is bounded by K1·diam s + K2·diam t.
Русский
Если для каждого b ∈ t отображение a ↦ f a b липшитцово на s с константой K1, и для каждого a ∈ s отображение b ↦ f a b липшицево на t с константой K2, то диаметр image2 f s t ограничен как K1·diam s + K2·diam t.
LaTeX
$$$\\text{ediam}(\\mathrm{image2} f\, s\, t) \\le K_1 \\operatorname{diam}(s) + K_2 \\operatorname{diam}(t)$$$
Lean4
theorem ediam_image2_le (f : α → β → γ) {K₁ K₂ : ℝ≥0} (s : Set α) (t : Set β)
(hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (f · b) s) (hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t) :
EMetric.diam (Set.image2 f s t) ≤ ↑K₁ * EMetric.diam s + ↑K₂ * EMetric.diam t :=
by
simp only [EMetric.diam_le_iff, forall_mem_image2]
intro a₁ ha₁ b₁ hb₁ a₂ ha₂ b₂ hb₂
refine (edist_triangle _ (f a₂ b₁) _).trans ?_
exact
add_le_add ((hf₁ b₁ hb₁ ha₁ ha₂).trans <| mul_right_mono <| EMetric.edist_le_diam_of_mem ha₁ ha₂)
((hf₂ a₂ ha₂ hb₁ hb₂).trans <| mul_right_mono <| EMetric.edist_le_diam_of_mem hb₁ hb₂)
