English
Under the local conditions, there exists a smooth function providing a global selection in the convex family.
Русский
При локальных условиях существует гладкая функция, обеспечивающая глобальный выбор из выпуклой семьи.
LaTeX
$$$\\exists f: Smooth( ... ), \\; f(x) ∈ t(x)\\; \\forall x$$$
Lean4
/-- Let `M` be a σ-compact Hausdorff finite-dimensional topological manifold. Let `t : M → Set F` be
a family of convex sets. Suppose that for each point `x : M` there exists a vector `c : F` such that
for all `y` in a neighborhood of `x` we have `c ∈ t y`. Then there exists a smooth function
`g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x ∈ t x` for all `x`. See also
`exists_contMDiffOn_forall_mem_convex_of_local` and `exists_smooth_forall_mem_convex_of_local`. -/
theorem exists_smooth_forall_mem_convex_of_local_const (ht : ∀ x, Convex ℝ (t x))
(Hloc : ∀ x : M, ∃ c : F, ∀ᶠ y in 𝓝 x, c ∈ t y) : ∃ g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x :=
exists_smooth_forall_mem_convex_of_local I ht fun x =>
let ⟨c, hc⟩ := Hloc x
⟨_, hc, fun _ => c, contMDiffOn_const, fun _ => id⟩
