English
In a topological vector space with separating dual and ContinuousSMul, the group of continuous linear equivalences acts transitively on nonzero vectors: given any nonzero x,y ∈ V there exists A ∈ GL(V) with A x = y.
Русский
В тегополном векторном пространстве с разделяющим двойственным и непрерывным действием умножения существует транзитивное действие группы непрерывных линейных взаимно обратимых отображений на ненулевых векторах: найдется A с A x = y.
LaTeX
$$$\exists A \in GL(V): A x = y$ для любых $x,y\neq 0$$$
Lean4
/-- A version of the **Hahn-Banach theorem**: given disjoint convex sets `s`, `t` where `s` is
compact and `t` is closed, there is a continuous linear functional which strongly separates them. -/
theorem geometric_hahn_banach_compact_closed (hs₁ : Convex ℝ s) (hs₂ : IsCompact s) (ht₁ : Convex ℝ t)
(ht₂ : IsClosed t) (disj : Disjoint s t) :
∃ (f : StrongDual ℝ E) (u v : ℝ), (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b :=
by
obtain rfl | hs := s.eq_empty_or_nonempty
· exact ⟨0, -2, -1, by simp⟩
obtain rfl | _ht := t.eq_empty_or_nonempty
· exact ⟨0, 1, 2, by simp⟩
obtain ⟨U, V, hU, hV, hU₁, hV₁, sU, tV, disj'⟩ := disj.exists_open_convexes hs₁ hs₂ ht₁ ht₂
obtain ⟨f, u, hf₁, hf₂⟩ := geometric_hahn_banach_open_open hU₁ hU hV₁ hV disj'
obtain ⟨x, hx₁, hx₂⟩ := hs₂.exists_isMaxOn hs f.continuous.continuousOn
have : f x < u := hf₁ x (sU hx₁)
exact
⟨f, (f x + u) / 2, u, fun a ha => by have := hx₂ ha; dsimp at this; linarith, by linarith, fun b hb =>
hf₂ b (tV hb)⟩
