geometric_hahn_banach_point_open — Mathlib

English

Given a convex open set s and a point x outside s, there exists a functional f distinguishing x from s with f(x) > f(s).

Русский

Для выпуклого открытого множества s и точки x вне s существует функционал f, который отделяет x от s: f(x) больше, чем значения на s.

LaTeX

$$$\exists f, \forall a\in s:\; f(a) < f(x)$$$

Lean4

theorem geometric_hahn_banach_point_open (ht₁ : Convex ℝ t) (ht₂ : IsOpen t) (disj : x ∉ t) :
    ∃ f : StrongDual ℝ E, ∀ b ∈ t, f x < f b :=
  let ⟨f, hf⟩ := geometric_hahn_banach_open_point ht₁ ht₂ disj
  ⟨-f, by simpa⟩

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