isBounded_iff_subset_smul_closedBall

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

Похожие утверждения