English
Let f: α → β → γ be such that for every b, the map a ↦ f(a,b) is AntilipschitzWith K₁. If Set.image2 f s t is bounded, then either s or t is bounded.
Русский
Пусть f: α → β → γ удовлетворяет условию: для каждого b отображение a ↦ f(a,b) является AntilipschitzWith K₁. Если Set.image2 f s t ограничено, то хотя бы одно из s, t ограничено.
LaTeX
$$$ \forall b, \operatorname{AntilipschitzWith} K_1 (\lambda a, 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_left (f : α → β → γ) {K₁ : ℝ≥0} (hf : ∀ b, AntilipschitzWith K₁ fun a => f a b) {s : Set α}
{t : Set β} (hst : IsBounded (Set.image2 f s t)) : IsBounded s ∨ IsBounded t :=
by
contrapose! hst
obtain ⟨b, hb⟩ : t.Nonempty := nonempty_of_not_isBounded hst.2
have : ¬IsBounded (Set.image2 f s { b }) := by
intro h
apply hst.1
rw [Set.image2_singleton_right] at h
replace h := (hf b).isBounded_preimage h
exact h.subset (subset_preimage_image _ _)
exact mt (IsBounded.subset · (image2_subset subset_rfl (singleton_subset_iff.mpr hb))) this
