contMDiffOn_comp_projIcc_iff — Mathlib

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

Похожие утверждения