Commit 2023-06-22 05:54 3c283adf

View on Github →

feat: port Analysis.Calculus.Implicit (#4665)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/Implicit.lean

added theorem HasStrictFDerivAt.eq_implicitFunction

added theorem HasStrictFDerivAt.eq_implicitFunctionOfComplemented

added def HasStrictFDerivAt.implicitFunction

added def HasStrictFDerivAt.implicitFunctionDataOfComplemented

added def HasStrictFDerivAt.implicitFunctionOfComplemented

added theorem HasStrictFDerivAt.implicitFunctionOfComplemented_apply_image

added theorem HasStrictFDerivAt.implicitFunction_apply_image

added def HasStrictFDerivAt.implicitToLocalHomeomorph

added def HasStrictFDerivAt.implicitToLocalHomeomorphOfComplemented

added theorem HasStrictFDerivAt.implicitToLocalHomeomorphOfComplemented_apply

added theorem HasStrictFDerivAt.implicitToLocalHomeomorphOfComplemented_apply_ker

added theorem HasStrictFDerivAt.implicitToLocalHomeomorphOfComplemented_fst

added theorem HasStrictFDerivAt.implicitToLocalHomeomorphOfComplemented_self

added theorem HasStrictFDerivAt.implicitToLocalHomeomorph_apply_ker

added theorem HasStrictFDerivAt.implicitToLocalHomeomorph_fst

added theorem HasStrictFDerivAt.implicitToLocalHomeomorph_self

added theorem HasStrictFDerivAt.map_implicitFunctionOfComplemented_eq

added theorem HasStrictFDerivAt.map_implicitFunction_eq

added theorem HasStrictFDerivAt.mem_implicitToLocalHomeomorphOfComplemented_source

added theorem HasStrictFDerivAt.mem_implicitToLocalHomeomorphOfComplemented_target

added theorem HasStrictFDerivAt.mem_implicitToLocalHomeomorph_source

added theorem HasStrictFDerivAt.mem_implicitToLocalHomeomorph_target

added theorem HasStrictFDerivAt.tendsto_implicitFunction

added theorem HasStrictFDerivAt.to_implicitFunction

added theorem HasStrictFDerivAt.to_implicitFunctionOfComplemented

added def ImplicitFunctionData.implicitFunction

added theorem ImplicitFunctionData.implicitFunction_apply_image

added theorem ImplicitFunctionData.implicitFunction_hasStrictFDerivAt

added theorem ImplicitFunctionData.left_map_implicitFunction

added theorem ImplicitFunctionData.map_nhds_eq

added theorem ImplicitFunctionData.map_pt_mem_toLocalHomeomorph_target

added def ImplicitFunctionData.prodFun

added theorem ImplicitFunctionData.prodFun_apply

added theorem ImplicitFunctionData.prod_map_implicitFunction

added theorem ImplicitFunctionData.pt_mem_toLocalHomeomorph_source

added theorem ImplicitFunctionData.right_map_implicitFunction

added def ImplicitFunctionData.toLocalHomeomorph

added theorem ImplicitFunctionData.toLocalHomeomorph_apply

added theorem ImplicitFunctionData.toLocalHomeomorph_coe

added structure ImplicitFunctionData