Separating two directions by a functional

Two vectors d₁ and d₂ of a real locally convex Hausdorff space with 0 ∉ [-d₁, d₂], that is, both nonzero and not on a common ray from 0, are separated by a continuous functional ℓ with ℓ d₁ < 0 < ℓ d₂. This is the geometric Hahn--Banach theorem geometric_hahn_banach_point_closed applied to the point 0 and the segment [-d₁, d₂]. Both strict inequalities are open conditions, so ℓ can moreover be perturbed to be nonzero at any prescribed vector on which some functional does not vanish.

Main results

• TauCeti.exists_strongDual_neg_pos_ne_zero: a functional negative on d₁, positive on d₂, and nonzero at a prescribed vector u.

theorem TauCeti.exists_strongDual_neg_pos_ne_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [T2Space E] {d₁ d₂ : E} (h : 0 ∉ segment ℝ (-d₁) d₂) (ℓ₀ : StrongDual ℝ E) {u : E} (hu : ℓ₀ u = 1) : ∃ (ℓ : StrongDual ℝ E), ℓ d₁ < 0 ∧ 0 < ℓ d₂ ∧ ℓ u ≠ 0

Two vectors with 0 ∉ [-d₁, d₂], that is nonzero and not on a common ray from 0, are separated by a continuous functional which is negative on d₁ and positive on d₂; it can be chosen nonzero at any vector u on which some functional ℓ₀ takes the value 1.