Asymptotic cones in normed spaces

In this file, we prove that the asymptotic cone of a set is non-trivial if and only if the set is unbounded.

theorem AffineSpace.asymptoticNhds_le_cobounded {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {v : V} (hv : v ≠ 0) : asymptoticNhds ℝ P v ≤ Bornology.cobounded P

theorem asymptoticCone_subset_singleton_of_bounded {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : Set P} (hs : Bornology.IsBounded s) : asymptoticCone ℝ s ⊆ {0}

theorem AffineSpace.cobounded_eq_iSup_sphere_asymptoticNhds {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [FiniteDimensional ℝ V] : Bornology.cobounded P = ⨆ v ∈ Metric.sphere 0 1, asymptoticNhds ℝ P v

theorem isBounded_iff_asymptoticCone_subset_singleton {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [FiniteDimensional ℝ V] {s : Set P} : Bornology.IsBounded s ↔ asymptoticCone ℝ s ⊆ {0}

In a finite dimensional normed affine space over ℝ, a set is bounded if and only if its asymptotic cone is trivial.

theorem not_bounded_iff_exists_ne_zero_mem_asymptoticCone {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [FiniteDimensional ℝ V] {s : Set P} : ¬Bornology.IsBounded s ↔ ∃ (v : 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.