English
Relates ContMDiffOn with ContMDiffWithinAt for projection onto Icc x y.
Русский
Связь ContMDiffOn и ContMDiffWithinAt через проекцию на Icc x y.
LaTeX
$$$\text{contMDiffOn_projIcc} \iff \text{contMDiffWithinAt for projection}$$$
Lean4
/-- The inclusion map from of a closed segment to `ℝ` is smooth in the manifold sense. -/
theorem contMDiff_subtype_coe_Icc : ContMDiff (𝓡∂ 1) 𝓘(ℝ) n (fun (z : Icc x y) ↦ (z : ℝ)) :=
by
intro z
rw [contMDiffAt_iff]
refine
⟨by fun_prop, ?_⟩
-- We come back to the definition: we should check that, in each chart, the map is smooth.
-- There are two charts, and we check things separately in each of them using the
-- explicit formulas.
suffices ContDiffWithinAt ℝ n _ (range ↑(𝓡∂ 1)) _ by simpa
split_ifs with hz
· simp? [IccLeftChart, Function.comp_def, modelWithCornersEuclideanHalfSpace] says
simp only [IccLeftChart, Fin.isValue, OpenPartialHomeomorph.mk_coe_symm, PartialEquiv.coe_symm_mk,
modelWithCornersEuclideanHalfSpace, ModelWithCorners.mk_symm, Function.comp_def, Function.update_self,
ModelWithCorners.mk_coe, OpenPartialHomeomorph.mk_coe]
rw [Subtype.range_val_subtype]
have : ContDiff ℝ n (fun (z : EuclideanSpace ℝ (Fin 1)) ↦ z 0 + x) := by fun_prop
apply this.contDiffWithinAt.congr_of_eventuallyEq_of_mem; swap
· simpa using z.2.1
have : {w : EuclideanSpace ℝ (Fin 1) | w 0 < y - x} ∈ 𝓝 (fun i ↦ z - x) :=
by
apply (isOpen_lt (continuous_apply 0) continuous_const).mem_nhds
simpa using hz
filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds this] with w hw h'w
rw [max_eq_left hw, min_eq_left]
linarith
· simp only [not_lt] at hz
simp? [IccRightChart, Function.comp_def, modelWithCornersEuclideanHalfSpace] says
simp only [IccRightChart, Fin.isValue, OpenPartialHomeomorph.mk_coe_symm, PartialEquiv.coe_symm_mk,
modelWithCornersEuclideanHalfSpace, ModelWithCorners.mk_symm, Function.comp_def, Function.update_self,
ModelWithCorners.mk_coe, OpenPartialHomeomorph.mk_coe]
rw [Subtype.range_val_subtype]
have : ContDiff ℝ n (fun (z : EuclideanSpace ℝ (Fin 1)) ↦ y - z 0) := by fun_prop
apply this.contDiffWithinAt.congr_of_eventuallyEq_of_mem; swap
· simpa using z.2.2
have : {w : EuclideanSpace ℝ (Fin 1) | w 0 < y - x} ∈ 𝓝 (fun i ↦ y - z) :=
by
apply (isOpen_lt (continuous_apply 0) continuous_const).mem_nhds
simpa using h.out.trans_le hz
filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds this] with w hw h'w
rw [max_eq_left hw, max_eq_left]
linarith
