lemma A.512 The boundary strip is thin
open in the book ·
appendices/A-long-proofs.tex:25003
· p. 3042
Rests on
-
depends_on
definition 7.127
Simple regions
¶
-
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 definition 7.2 Absolute value ¶
- depends_on definition 7.9 Real function ¶
- depends_on equation 7.7 eq:ana-limit-left ¶
- depends_on equation 7.5 eq:ana-limit-right ¶
-
depends_on
definition 7.16
Limit
¶
-
depends_on
definition 7.97
Partial derivative; gradient
¶
-
depends_on
definition 7.26
Derivative of a function at a point
¶
- depends_on definition 7.16 Limit ¶ ↺
- depends_on definition 7.9 Real function ¶ ↺
-
depends_on
definition 5.15
Basis
¶
- depends_on definition 5.12 Subspace generated by a set of vectors ¶
- depends_on definition 5.14 Linear independence ¶
-
depends_on
definition 7.26
Derivative of a function at a point
¶
-
depends_on
definition 7.20
Continuity at a point
¶
-
depends_on
definition 6.9
Compact set
¶
-
depends_on
definition 6.5
Open cover
¶
-
depends_on
definition 6.2
Open set
¶
- depends_on definition 6.1 Topological space ¶
- depends_on equation 3.51 eq:set-indexed ¶
-
depends_on
definition 6.2
Open set
¶
-
depends_on
definition 6.5
Open cover
¶
-
depends_on
definition 7.98
Functions of class $C^{1}$
¶
-
depends_on
lemma A.500
Graphs and $C^{1}$ images have zero content
¶
-
depends_on
lemma A.499
What zero content buys
¶
-
depends_on
definition 7.125
Multiple integral
¶
- depends_on axiom 7.1 Completeness of $\R$ ¶
-
depends_on
definition 7.39
Darboux sums and the definite integral
¶
- depends_on axiom 7.1 Completeness of $\R$ ¶ ↺
-
depends_on
definition A.498
Zero content
¶
- depends_on definition 7.125 Multiple integral ¶ ↺
- depends_on definition 6.9 Compact set ¶ ↺
-
depends_on
theorem 7.25
Heine–Cantor: uniform continuity
¶
-
depends_on
proposition 7.22
Sequential characterization
¶
- depends_on definition 7.20 Continuity at a point ¶ ↺
- depends_on definition 7.4 Convergence ¶
- proves proof ch:05-real-analysis@proof-7 ¶
-
depends_on
theorem 7.7
Bolzano–Weierstrass
¶
- depends_on corollary A.45 Archimedean property and density of $\Q$ ¶
- depends_on corollary A.46 Monotone convergence ¶
- proves proof ch:05-real-analysis@proof-4 ¶
- proves proof ch:05-real-analysis@proof-10 ¶
-
depends_on
proposition 7.22
Sequential characterization
¶
- proves proof app:A-long-proofs@proof-295 ¶
-
depends_on
definition 7.125
Multiple integral
¶
- depends_on theorem 7.25 Heine–Cantor: uniform continuity ¶ ↺
-
depends_on
theorem 7.35
Mean value theorem
¶
-
depends_on
proposition 7.29
Linearity
¶
-
depends_on
definition 7.11
Sum of functions
¶
- depends_on definition 7.9 Real function ¶ ↺
- depends_on equation 7.14 eq:ana-derivh ¶
-
depends_on
proposition 7.6
Algebra of limits
¶
- depends_on definition 7.4 Convergence ¶ ↺
- depends_on proposition 7.3 Triangle inequality ¶
- proves proof ch:05-real-analysis@proof-3 ¶
- proves proof ch:05-real-analysis@proof-13 ¶
-
depends_on
definition 7.11
Sum of functions
¶
-
depends_on
theorem 7.34
Rolle
¶
-
depends_on
lemma 7.33
Fermat: interior extremum
¶
- depends_on definition 7.26 Derivative of a function at a point ¶ ↺
- depends_on proposition 7.18 Two-sided limit from one-sided limits ¶
- proves proof ch:05-real-analysis@proof-17 ¶
-
depends_on
theorem 7.24
Extreme value theorem
¶
- depends_on axiom 7.1 Completeness of $\R$ ¶ ↺
- depends_on proposition 7.22 Sequential characterization ¶ ↺
- depends_on theorem 7.7 Bolzano–Weierstrass ¶ ↺
- proves proof ch:05-real-analysis@proof-9 ¶
- proves proof ch:05-real-analysis@proof-18 ¶
-
depends_on
lemma 7.33
Fermat: interior extremum
¶
- proves proof ch:05-real-analysis@proof-19 ¶
-
depends_on
proposition 7.29
Linearity
¶
- proves proof app:A-long-proofs@proof-296 ¶
-
depends_on
lemma A.499
What zero content buys
¶
- depends_on theorem 7.25 Heine–Cantor: uniform continuity ¶ ↺
- proves proof app:A-long-proofs@proof-306 ¶
Supports
-
depends_on
theorem A.513
Change of variables
¶
- depends_on corollary A.514 Degeneracy on a negligible set ¶
- depends_on remark A.516 The hypotheses of the global form ¶
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 |
→ | Simple regions | declared | appendices/A-long-proofs.tex:25016 |
depends_on |
→ | Graphs and $C^{1}$ images have zero content | declared | appendices/A-long-proofs.tex:25016 |
depends_on |
→ | Heine–Cantor: uniform continuity | declared | appendices/A-long-proofs.tex:25016 |
depends_on |
← | Change of variables | declared | appendices/A-long-proofs.tex:25046 |
proves |
← | app:A-long-proofs@proof-306 | declared | appendices/A-long-proofs.tex:25020 |