geometric_hahn_banach_open — Mathlib

English

In the RCLike setting, there exists a StrongDual functional with real part separation at a point outside an open convex set.

Русский

В рамках RCLike существует функционал StrongDual, для которого вещественная часть разделяет точку за пределами открытого выпуклого множества.

LaTeX

$$$\exists f:\; \forall a\in s:\; \mathrm{re}(f(a)) < \mathrm{re}(f(x))$$$

Lean4

theorem geometric_hahn_banach_open (hs₁ : Convex ℝ s) (hs₂ : IsOpen s) (ht : Convex ℝ t) (disj : Disjoint s t) :
    ∃ (f : StrongDual 𝕜 E) (u : ℝ), (∀ a ∈ s, re (f a) < u) ∧ ∀ b ∈ t, u ≤ re (f b) :=
  by
  have := IsScalarTower.continuousSMul (M := ℝ) (α := E) 𝕜
  obtain ⟨f, u, h⟩ := _root_.geometric_hahn_banach_open hs₁ hs₂ ht disj
  use extendTo𝕜'ₗ f
  simp only [re_extendTo𝕜'ₗ]
  exact Exists.intro u h

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