isVonNBounded_of_isBounded — Mathlib

English

The union of all vonNBounded sets equals the whole space (variant statement).

Русский

Объединение всех ограниченных фон Нейманом множеств равно всему пространству (вариант утверждения).

LaTeX

$$$⋃_{X:\\mathrm{Set}\\;}{\\ IsVonNBounded}(X) = \\mathrm{univ}$$$

Lean4

theorem isVonNBounded_of_isBounded {s : Set E} (h : Bornology.IsBounded s) : Bornology.IsVonNBounded 𝕜 s :=
  by
  rcases h.subset_ball 0 with ⟨r, hr⟩
  rw [Metric.nhds_basis_ball.isVonNBounded_iff]
  rw [← ball_normSeminorm 𝕜 E] at hr ⊢
  exact fun ε hε ↦ ((normSeminorm 𝕜 E).ball_zero_absorbs_ball_zero hε).mono_right hr

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