geometric_hahn_banach_open_point — Mathlib

English

If s and t are disjoint convex open sets in E, there exists a functional separating them: either f(a) < u for all a ∈ s and u < f(b) for all b ∈ t.

Русский

Пусть s и t — несмежные выпуклые открытые множества; существует функционал, разделяющий их (один порог между ними).

LaTeX

$$$\exists f,\exists u:\; (\forall a\in s:\; f(a) < u) \land (\forall b\in t:\; u < f(b))$$$

Lean4

theorem geometric_hahn_banach_open_point (hs₁ : Convex ℝ s) (hs₂ : IsOpen s) (disj : x ∉ s) :
    ∃ f : StrongDual ℝ E, ∀ a ∈ s, f a < f x :=
  let ⟨f, _s, hs, hx⟩ := geometric_hahn_banach_open hs₁ hs₂ (convex_singleton x) (disjoint_singleton_right.2 disj)
  ⟨f, fun a ha => lt_of_lt_of_le (hs a ha) (hx x (mem_singleton _))⟩

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