English
For any f: Icc x y → M, ContMDiffOn (I, I) on Icc x y is equivalent to ContMDiff on the image side after projecting.
Русский
Для любого f: Icc x y → M: ContMDiffOn после проекции эквивалентно ContMDiff на образе.
LaTeX
$$$\forall f, ContMDiffOn (modelWithCornersSelf Real Real) I n (Function.comp f (Set.projIcc x y ⋯)) (Set.Icc x y) w \iff ContMDiff (modelWithCornersEuclideanHalfSpace 1) I n f$$$
Lean4
theorem contMDiffOn_comp_projIcc_iff {f : Icc x y → M} :
ContMDiffOn 𝓘(ℝ) I n (f ∘ (Set.projIcc x y h.out.le)) (Icc x y) ↔ ContMDiff (𝓡∂ 1) I n f :=
by
refine ⟨fun hf ↦ ?_, fun hf ↦ hf.comp_contMDiffOn contMDiffOn_projIcc⟩
convert hf.comp_contMDiff (contMDiff_subtype_coe_Icc (x := x) (y := y)) (fun z ↦ z.2)
ext z
simp