lemma A.290 $h$ is Lipschitz
open in the book ·
appendices/A-long-proofs.tex:14543
· p. 2935
Rests on
-
depends_on
lemma A.288
The iteration converges
¶
-
depends_on
lemma A.287
The Newton map contracts
¶
-
depends_on
definition 7.98
Functions of class $C^{1}$
¶
-
depends_on
definition 7.20
Continuity at a point
¶
- depends_on definition 7.16 Limit ¶
- depends_on equation 7.7 eq:ana-limit-left ¶
- depends_on equation 7.5 eq:ana-limit-right ¶
-
depends_on
definition 7.97
Partial derivative; gradient
¶
- depends_on definition 7.26 Derivative of a function at a point ¶
- depends_on definition 5.15 Basis ¶
-
depends_on
definition 7.20
Continuity at a point
¶
- depends_on equation A.523 eq:app-implicit-hypothesis ¶
-
depends_on
theorem 7.35
Mean value theorem
¶
-
depends_on
proposition 7.29
Linearity
¶
- depends_on definition 7.11 Sum of functions ¶
- depends_on equation 7.14 eq:ana-derivh ¶
- depends_on proposition 7.6 Algebra of limits ¶
- proves proof ch:05-real-analysis@proof-13 ¶
-
depends_on
theorem 7.34
Rolle
¶
- depends_on lemma 7.33 Fermat: interior extremum ¶
- depends_on theorem 7.24 Extreme value theorem ¶
- proves proof ch:05-real-analysis@proof-18 ¶
- proves proof ch:05-real-analysis@proof-19 ¶
-
depends_on
proposition 7.29
Linearity
¶
- proves proof app:A-long-proofs@proof-180 ¶
-
depends_on
definition 7.98
Functions of class $C^{1}$
¶
-
depends_on
proposition 7.46
Geometric series
¶
-
depends_on
corollary A.46
Monotone convergence
¶
-
depends_on
theorem A.40
Least-upper-bound property
¶
- depends_on definition A.36 Cut ¶
- depends_on definition A.38 Order on $\R$ ¶
- proves proof app:A-long-proofs@proof-29 ¶
- proves proof app:A-long-proofs@proof-33 ¶
-
depends_on
theorem A.40
Least-upper-bound property
¶
-
depends_on
definition 7.45
Series
¶
- depends_on definition 7.2 Absolute value ¶
-
depends_on
definition 7.4
Convergence
¶
- depends_on definition 7.2 Absolute value ¶ ↺
- proves proof ch:05-real-analysis@proof-27 ¶
-
depends_on
corollary A.46
Monotone convergence
¶
-
depends_on
theorem 7.8
Cauchy criterion
¶
-
depends_on
corollary A.47
Cauchy completeness
¶
- depends_on corollary A.46 Monotone convergence ¶ ↺
- depends_on theorem A.40 Least-upper-bound property ¶ ↺
- proves proof app:A-long-proofs@proof-34 ¶
- depends_on definition 7.4 Convergence ¶ ↺
- proves proof ch:05-real-analysis@proof-5 ¶
-
depends_on
corollary A.47
Cauchy completeness
¶
- proves proof app:A-long-proofs@proof-181 ¶
-
depends_on
lemma A.287
The Newton map contracts
¶
- depends_on theorem 7.35 Mean value theorem ¶ ↺
- proves proof app:A-long-proofs@proof-183 ¶
Supports
- depends_on lemma A.291 $h$ is differentiable, with the stated derivative ¶
Neighborhood
Every logical edge within two steps of this node.
- declared and complete
- partly declared
- a check failed
- not graded
- declared in the source
- inferred from structure
Edges
| type | direction | node | provenance | where |
|---|---|---|---|---|
depends_on |
→ | The iteration converges | declared | appendices/A-long-proofs.tex:14549 |
depends_on |
→ | Mean value theorem | declared | appendices/A-long-proofs.tex:14549 |
depends_on |
← | $h$ is differentiable, with the stated derivative | declared | appendices/A-long-proofs.tex:14587 |
proves |
← | app:A-long-proofs@proof-183 | declared | appendices/A-long-proofs.tex:14552 |