English
Let X be a normal paracompact space and E a real vector space. If for each x there exists a neighborhood U and continuous g: X→E with g(y) ∈ t(y) for all y ∈ U, and t(y) is convex for each y, then there exists a global continuous g with g(x) ∈ t(x) for all x.
Русский
Пусть X нормальное паракомпактное пространство, E—реальное векторное пространство. Если для каждого x существует окрестность U и непрерывная функция g: X→E, такая что g(y) ∈ t(y) для всех y ∈ U, и t(y) выпукло для каждого y, то существует глобальная непрерывная функция 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 neighborhood `U ∈ 𝓝 X` and a function `g : X → E` that is
continuous on `U` and sends each `y ∈ U` to a point of `t y`. 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_const`. -/
theorem exists_continuous_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t x))
(H : ∀ x : X, ∃ U ∈ 𝓝 x, ∃ g : X → E, ContinuousOn g U ∧ ∀ y ∈ U, g y ∈ t y) : ∃ g : C(X, E), ∀ x, g x ∈ t x :=
by
choose U hU g hgc hgt using H
obtain ⟨f, hf⟩ :=
PartitionOfUnity.exists_isSubordinate isClosed_univ (fun x => interior (U x)) (fun x => isOpen_interior) fun x _ =>
mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x)⟩
refine
⟨⟨fun x => ∑ᶠ i, f i x • g i x,
hf.continuous_finsum_smul (fun i => isOpen_interior) fun i => (hgc i).mono interior_subset⟩,
fun x => f.finsum_smul_mem_convex (mem_univ x) (fun i hi => hgt _ _ ?_) (ht _)⟩
exact interior_subset (hf _ <| subset_closure hi)
