contMDiffWithinAt_comp_projIcc_iff

English

MDifferentiableWithinAt with projection on Icc is equivalent to MDifferentiableAt of f at w.

Русский

MDifferentiableWithinAt с проекцией на Icc эквивалентно MDifferentiableAt функции f в w.

LaTeX

$$$\text{MDifferentiableWithinAt } 𝓘(ℝ) I n (f ∘ (Set.projIcc x y h.out.le)) (Icc x y) w \iff MDifferentiableAt (𝓡∂ 1) I f w$$$

Lean4

theorem contMDiffWithinAt_comp_projIcc_iff {f : Icc x y → M} {w : Icc x y} :
    ContMDiffWithinAt 𝓘(ℝ) I n (f ∘ (Set.projIcc x y h.out.le)) (Icc x y) w ↔ ContMDiffAt (𝓡∂ 1) I n f w :=
  by
  refine ⟨fun hf ↦ ?_, fun hf ↦ hf.comp_contMDiffWithinAt_of_eq (contMDiffOn_projIcc w w.2) (by simp)⟩
  have A := contMDiff_subtype_coe_Icc (x := x) (y := y) (n := n) w
  rw [← contMDiffWithinAt_univ] at A ⊢
  convert hf.comp _ A (fun z hz ↦ z.2)
  ext z
  simp

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