isBounded_iff_forall_norm_le' — Mathlib

English

IsBounded s is equivalent to the existence of a bound C for all x in s: ∥x∥ ≤ C.

Русский

IsBounded s эквивалентно существованию границы C для всех x в s: ∥x∥ ≤ C.

LaTeX

$$Bornology.IsBounded s ↔ ∃ C, ∀ x ∈ s, ∥x∥ ≤ C$$

Lean4

@[to_additive isBounded_iff_forall_norm_le]
theorem isBounded_iff_forall_norm_le' : Bornology.IsBounded s ↔ ∃ C, ∀ x ∈ s, ‖x‖ ≤ C := by
  simpa only [Set.subset_def, mem_closedBall_one_iff] using isBounded_iff_subset_closedBall (1 : E)

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