differentiableWithinAtProp_self_target

English

If f is differentiable within at, then its written-in-ext-chart-at version is differentiable within at on the chart domain.

Русский

Если функция дифференцируема внутри множества, то её запись в расширенной координатной карте дифференцируема на области карты.

LaTeX

$$$\text{mdifferentiableWithinAt_writtenInExtChartAt } (f) :\text{ DifferentiableWithinAt } 𝕜 (writtenInExtChartAt I I' x f) (\text{range } I) ((\text{extChartAt } I x) x)$$$

Lean4

theorem differentiableWithinAtProp_self_target {f : H → E'} {s : Set H} {x : H} :
    DifferentiableWithinAtProp I 𝓘(𝕜, E') f s x ↔
      DifferentiableWithinAt 𝕜 (f ∘ I.symm) (I.symm ⁻¹' s ∩ range I) (I x) :=
  Iff.rfl

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