English
The dual cone of the empty set is the top/entire cone.
Русский
Двойной конус пустого множества равен всем пространство.
LaTeX
$$$\\text{innerDual}(\\emptyset)=\\top$$$
Lean4
/-- Relative geometric interpretation of **Farkas' lemma**. Also stronger version of the
**Hahn-Banach separation theorem** for proper cones. -/
theorem relative_hyperplane_separation {C : ProperCone ℝ E} {f : E →L[ℝ] F} {b : F} :
b ∈ C.map f ↔ ∀ y : F, f.adjoint y ∈ innerDual C → 0 ≤ ⟪b, y⟫_ℝ
where
mp := by
-- suppose `b ∈ C.map f`
simp only [map, ClosedSubmodule.map, Submodule.closure, Submodule.topologicalClosure,
AddSubmonoid.topologicalClosure, Submodule.coe_toAddSubmonoid, Submodule.map_coe,
ContinuousLinearMap.coe_restrictScalars', ClosedSubmodule.coe_toSubmodule, ClosedSubmodule.mem_mk,
Submodule.mem_mk, AddSubmonoid.mem_mk, AddSubsemigroup.mem_mk, mem_closure_iff_seq_limit, mem_image,
SetLike.mem_coe, Classical.skolem, forall_and, mem_innerDual, ContinuousLinearMap.adjoint_inner_right,
forall_exists_index, and_imp]
-- there is a sequence `seq : ℕ → F` in the image of `f` that converges to `b`
rintro x seq hmem hx htends y hinner
obtain rfl : f ∘ seq = x := funext hx
have h n : 0 ≤ ⟪f (seq n), y⟫_ℝ := by simpa [real_inner_comm] using hinner (hmem n)
exact ge_of_tendsto' ((continuous_id.inner continuous_const).seqContinuous htends) h
mpr
h := by
-- By contradiction, suppose `b ∉ C.map f`.
contrapose! h
obtain ⟨y, hxy, hyb⟩ := (C.map f).hyperplane_separation' h
refine ⟨y, fun x hx ↦ ?_, hyb⟩
simpa [ContinuousLinearMap.adjoint_inner_right] using hxy (f x) (subset_closure <| mem_image_of_mem _ hx)
