Theorems · Theorem · functional analysis

not_bounded_iff_exists_ne_zero_mem_asymptoticCone

∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [FiniteDimensional ℝ V] {s : Set P},
  ¬Bornology.IsBounded s ↔ ∃ v, v ≠ 0 ∧ v ∈ asymptoticCone ℝ s

In a finite dimensional normed affine space over ℝ, a set is unbounded if and only if its asymptotic cone contains a nonzero vector.

Defined in

Mathlib.Analysis.Normed.Affine.AsymptoticCone

Cited by

0 results in Mathlib

Foundations

Depth 180 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceMetricSpaceNormedAddTorsorFiniteDimensional