Hahn--Banach separation above a closed cone

This is the analytic step used in the reconstructed infinite version of Scott's Theorem 4.1. A closed convex set which is stable under translation by a closed cone and avoids zero admits a functional which is nonnegative on the cone and strictly positive on the set.

def Scott1964.MeasurementStructures.Probability.Infinite.ConeUpperSet {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (C : ProperCone ℝ E) (K : Set E) : Prop

K is upward closed under translation by the cone C.

Equations

• Scott1964.MeasurementStructures.Probability.Infinite.ConeUpperSet C K = ∀ ⦃x c : E⦄, x ∈ K → c ∈ C → x + c ∈ K

theorem Scott1964.MeasurementStructures.Probability.Infinite.exists_positive_separator_of_coneUpper {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [LocallyConvexSpace ℝ E] (C : ProperCone ℝ E) {K : Set E} (hKne : K.Nonempty) (hKconv : Convex ℝ K) (hKclosed : IsClosed K) (hKzero : 0 ∉ K) (hupper : ConeUpperSet C K) : ∃ (f : StrongDual ℝ E), (∀ c ∈ C, 0 ≤ f c) ∧ ∀ x ∈ K, 0 < f x

The Hahn--Banach separation lemma in the exact form needed for Kelley's countable-cover argument.