English
In a normal paracompact space, if at every point there is a local convex neighborhood of E-valued selections, then there exists a global continuous selection g with g(x) ∈ t(x) for all x.
Русский
В нормальном парекомпактном пространстве, если вокруг каждого точки имеется локальный выпуклый выбор, то существует глобальная непрерывная выборка g с g(x) ∈ t(x) для всех x.
LaTeX
$$$\exists g: C(X,E), \forall x: X, g(x) \in t(x)$$$
Lean4
/-- Let `X` be a normal paracompact topological space (e.g., any extended metric space). Let `E` be
a topological real vector space. Let `t : X → Set E` be a family of convex sets. Suppose that for
each point `x : X`, there exists a vector `c : E` that belongs to `t y` for all `y` in a
neighborhood of `x`. Then there exists a continuous map `g : C(X, E)` such that `g x ∈ t x` for all
`x`. See also `exists_continuous_forall_mem_convex_of_local`. -/
theorem exists_continuous_forall_mem_convex_of_local_const (ht : ∀ x, Convex ℝ (t x))
(H : ∀ x : X, ∃ c : E, ∀ᶠ y in 𝓝 x, c ∈ t y) : ∃ g : C(X, E), ∀ x, g x ∈ t x :=
exists_continuous_forall_mem_convex_of_local ht fun x =>
let ⟨c, hc⟩ := H x
⟨_, hc, fun _ => c, continuousOn_const, fun _ => id⟩
