unbounded_univ — Mathlib

English

In a nontrivial normed space E, the whole space E is not a bounded set; i.e., E is not bounded as a subset of itself.

Русский

Во множестве ненулевого нормированного пространства E пространство E не является ограниченным подмножеством самого себя.

LaTeX

$$$\\neg \\operatorname{IsBounded}(\\mathrm{univ} : \\mathrm{Set} E)$$$

Lean4

protected theorem unbounded_univ : ¬Bornology.IsBounded (univ : Set E) := fun h =>
  let ⟨R, hR⟩ := isBounded_iff_forall_norm_le.1 h
  let ⟨x, hx⟩ := NormedSpace.exists_lt_norm 𝕜 E R
  hx.not_ge (hR x trivial)

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