Theorems · Theorem · global analysis

HasStrictFDerivAt.localInverse.congr_simp

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f f_1 : E → F)
  (e_f : f = f_1) (f' f'_1 : E ≃L[𝕜] F) (e_f' : f' = f'_1) (a a_1 : E) (e_a : a = a_1) [inst_5 : CompleteSpace E]
  (hf : HasStrictFDerivAt f (↑f') a) (a_2 a_3 : F),
  a_2 = a_3 → HasStrictFDerivAt.localInverse f f' a hf a_2 = HasStrictFDerivAt.localInverse f_1 f'_1 a_1 ⋯ a_3

Defined in

Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv

Cited by

0 results in Mathlib

Foundations

Depth 185 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceCompleteSpace