English
There exists a functional f and a threshold u separating a point x from a set s (open convex), with f(x) < u and f(s) < u.
Русский
Существует функционал f и пороговое значение u, разделяющее точку x от открытого выпуклого множества s, причем f(x) < u и f(s) < u.
LaTeX
$$$\exists f,u:\; \forall a\in s:\; f(a) < u \land f(x) < u$$$
Lean4
theorem geometric_hahn_banach_open_open (hs₁ : Convex ℝ s) (hs₂ : IsOpen s) (ht₁ : Convex ℝ t) (ht₃ : IsOpen t)
(disj : Disjoint s t) : ∃ (f : StrongDual ℝ E) (u : ℝ), (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u < f b :=
by
obtain rfl | ⟨a₀, ha₀⟩ := s.eq_empty_or_nonempty
· exact ⟨0, -1, by simp, fun b _hb => by simp⟩
obtain rfl | ⟨b₀, hb₀⟩ := t.eq_empty_or_nonempty
· exact ⟨0, 1, fun a _ha => by simp, by simp⟩
obtain ⟨f, s, hf₁, hf₂⟩ := geometric_hahn_banach_open hs₁ hs₂ ht₁ disj
refine ⟨f, s, hf₁, image_subset_iff.1 (?_ : f '' t ⊆ Ioi s)⟩
rw [← interior_Ici]
refine interior_maximal (image_subset_iff.2 hf₂) (f.isOpenMap_of_ne_zero ?_ _ ht₃)
rintro rfl
simp_rw [ContinuousLinearMap.zero_apply] at hf₁ hf₂
exact (hf₁ _ ha₀).not_ge (hf₂ _ hb₀)
