English
A set is bounded iff it is contained in a scaled ball around zero.
Русский
Множество ограничено по фон Нейману тогда, когда оно содержится в умноженном шаре вокруг нуля.
LaTeX
$$$\\operatorname{IsBounded}_{\\mathbb{k}}(s) \\iff \\exists a \\in \\mathbb{k},\\; s \\subseteq a \\cdot \\mathrm{Metric.ball}(0,1)$$$
Lean4
theorem isBounded_iff_subset_smul_closedBall {s : Set E} :
Bornology.IsBounded s ↔ ∃ a : 𝕜, s ⊆ a • Metric.closedBall (0 : E) 1 :=
by
constructor
· rw [isBounded_iff_subset_smul_ball 𝕜]
exact Exists.imp fun a ha => ha.trans <| Set.smul_set_mono <| Metric.ball_subset_closedBall
· rw [← isVonNBounded_iff 𝕜]
rintro ⟨a, ha⟩
exact ((isVonNBounded_closedBall 𝕜 E 1).image (a • (1 : E →L[𝕜] E))).subset ha