English
There exists a smooth section that takes values in convex fiber sets; this follows from the partition of unity construction.
Русский
Существует гладкая секция, принимающая значения в выпуклых множеств волокон; следует из построения разбиения единиц.
LaTeX
$$$\\exists s: C^\\infty\\text{-section},\\; s(x) \\in 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 neighborhood
`U ∈ 𝓝 x` and a function `g : M → F` such that `g` is $C^n$ smooth on `U` and `g y ∈ t y` for all
`y ∈ U`. Then there exists a $C^n$ smooth function `g : C^n⟮I, M; 𝓘(ℝ, F), F⟯` such that `g x ∈ t x`
for all `x`.
This is a special case of `exists_contMDiffOn_section_forall_mem_convex_of_local` where `V` is the
trivial bundle. See also `exists_smooth_forall_mem_convex_of_local` and
`exists_smooth_forall_mem_convex_of_local_const`. -/
theorem exists_contMDiffOn_forall_mem_convex_of_local (ht : ∀ x, Convex ℝ (t x))
(Hloc : ∀ x : M, ∃ U ∈ 𝓝 x, ∃ g : M → F, ContMDiffOn I 𝓘(ℝ, F) n g U ∧ ∀ y ∈ U, g y ∈ t y) :
∃ g : C^n⟮I, M; 𝓘(ℝ, F), F⟯, ∀ x, g x ∈ t x :=
let ⟨s, hs⟩ :=
exists_contMDiffOn_section_forall_mem_convex_of_local I (fun _ ↦ F) t ht
(fun x₀ ↦
let ⟨U, hU, g, hgs, hgt⟩ := Hloc x₀
⟨U, hU, g, fun y hy ↦ Bundle.contMDiffWithinAt_section |>.mpr <| hgs y hy, hgt⟩)
⟨⟨s, (Bundle.contMDiffAt_section _ |>.mp <| s.contMDiff ·)⟩, hs⟩
