English
There exists a contMDiffOn section selecting from convex fiber sets, under local hypotheses.
Русский
Существет contMDiffOn секция, выбирающая из выпуклых множеств волокон, при локальных предпосылках.
LaTeX
$$$\\exists s: ContMDiffOn\\, I\\, (𝓘(ℝ,F)) n\\, g,\\; s(y) \\subset t(y)$$$
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 neighborhood
`U ∈ 𝓝 x` and a function `g : M → F` such that `g` is smooth on `U` and `g y ∈ t y` for all `y ∈ U`.
Then there exists a smooth function `g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x ∈ t x` for all `x`.
This is a special case of `exists_smooth_section_forall_mem_convex_of_local` where `V` is the
trivial bundle. See also `exists_contMDiffOn_forall_mem_convex_of_local` and
`exists_smooth_forall_mem_convex_of_local_const`. -/
theorem exists_smooth_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t x))
(Hloc : ∀ x : M, ∃ U ∈ 𝓝 x, ∃ g : M → F, ContMDiffOn I 𝓘(ℝ, F) ∞ g U ∧ ∀ y ∈ U, g y ∈ t y) :
∃ g : C^∞⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x :=
exists_contMDiffOn_forall_mem_convex_of_local I ht Hloc
