Theorems · Theorem · convex and discrete geometry

ProperCone.hyperplane_separation

∀ {E : Type u_1} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [IsTopologicalAddGroup E] [inst_3 : Module ℝ E]
  [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {K : Set E} (C : ProperCone ℝ E),
  Convex ℝ K → IsCompact K → Disjoint K ↑C → ∃ f, (∀ x ∈ C, 0 ≤ f x) ∧ ∀ x ∈ K, f x < 0

Geometric interpretation of Farkas' lemma. Also stronger version of the Hahn-Banach separation theorem for proper cones.

Defined in

Mathlib.Analysis.Convex.Cone.Dual

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddCommGroupIsTopologicalAddGroupModuleContinuousSMulLocallyConvexSpace