geometric_hahn_banach_point_closed

English

For a convex closed set s and a non-member x, there exists a functional f which separates x from s with f x < f y for y ∈ s.

Русский

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

LaTeX

$$$\exists f,u:\; f(x) < u \land \forall y\in s:\; u < f(y)$$$

Lean4

theorem geometric_hahn_banach_point_closed (ht₁ : Convex ℝ t) (ht₂ : IsClosed t) (disj : x ∉ t) :
    ∃ (f : StrongDual ℝ E) (u : ℝ), f x < u ∧ ∀ b ∈ t, u < f b :=
  let ⟨f, _u, v, ha, hst, hb⟩ :=
    geometric_hahn_banach_compact_closed (convex_singleton x) isCompact_singleton ht₁ ht₂
      (disjoint_singleton_left.2 disj)
  ⟨f, v, hst.trans' <| ha x <| mem_singleton _, hb⟩

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