hyperplane_separation_of_notMem — Mathlib

English

If b is not in the image of a cone under map f, there exists a separating hyperplane y with adjoint in innerDual and ⟪b,y⟫ < 0.

Русский

Если b не принадлежит образу конуса C под отображением f, существует разделяющая гиперплоскость y, сопряжение которой лежит в innerDual и ⟪b,y⟫ < 0.

LaTeX

$$$\\neg(b\\in C.map f)\\Rightarrow \\exists y, (y\\in innerDual(C)) \\land \\langle b,y\\rangle<0$$$

Lean4

theorem hyperplane_separation_of_notMem (K : ProperCone ℝ E) {f : E →L[ℝ] F} {b : F} (disj : b ∉ K.map f) :
    ∃ y : F, ContinuousLinearMap.adjoint f y ∈ innerDual K ∧ ⟪b, y⟫_ℝ < 0 := by contrapose! disj;
  rwa [K.relative_hyperplane_separation]

Похожие утверждения