mdifferentiableWithinAt_of_isInvertible_mfderivWithin

English

Alternative expression: invertible mfderiv implies mdifferentiableAt.

Русский

Альтернативное выражение: обратно-множество mfderiv приводит к mdifferentiableAt.

LaTeX

$$$(mfderiv I I' f x).IsInvertible → MDifferentiableAt I I' f x$$$

Lean4

theorem mdifferentiableWithinAt_of_isInvertible_mfderivWithin (hf : (mfderivWithin I I' f s x).IsInvertible) :
    MDifferentiableWithinAt I I' f s x := by
  contrapose hf
  rw [mfderivWithin_zero_of_not_mdifferentiableWithinAt hf]
  contrapose! hf
  rcases ContinuousLinearMap.isInvertible_zero_iff.1 hf with ⟨hE, hF⟩
  have : Subsingleton E := hE
  exact mdifferentiable_of_subsingleton.mdifferentiableAt.mdifferentiableWithinAt

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