Analytic

📁 Source: Mathlib/Analysis/Calculus/InverseFunctionTheorem/Analytic.lean

Statistics

Metric	Count
Definitions	0
Theorems analyticAt_localInverse, analyticAt_comp_iff_of_deriv_ne_zero	2
Total	2

AnalyticAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticAt_localInverse 📖	mathematical	AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	HasStrictDerivAt.localInverse deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace hasStrictDerivAt	—	RingHomInvPair.ids IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasStrictDerivAt HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source HasFPowerSeriesAt.analyticAt OpenPartialHomeomorph.hasFPowerSeriesAt_symm hasFPowerSeriesAt ContinuousMultilinearMap.ext_ring Finite.of_fintype RingHomIsometric.ids smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul SeminormedAddCommGroup.toIsTopologicalAddGroup FormalMultilinearSeries.apply_eq_prod_smul_coeff Finset.prod_congr Finset.univ_unique Finset.prod_const_one FormalMultilinearSeries.coeff_ofScalars iteratedDeriv_one Nat.cast_one div_one one_mul

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticAt_comp_iff_of_deriv_ne_zero 📖	—	AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace	—	—	AnalyticAt.hasStrictDerivAt AnalyticAt.analyticAt_localInverse HasStrictFDerivAt.localInverse_apply_image HasStrictDerivAt.hasStrictFDerivAt_equiv AnalyticAt.congr AnalyticAt.comp Filter.EventuallyEq.fun_comp HasStrictDerivAt.eventually_right_inverse

---

← Back to Index