theorem A.303 Change of variables for multiple integrals; quoted
open in the book ·
appendices/A-long-proofs.tex:15004
· p. 2940
Rests on
-
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
remark 7.128
What the derivations below take as given
¶
- depends_on definition 7.125 Multiple integral ¶ ↺
-
depends_on
theorem 7.40
Continuous functions are integrable
¶
- depends_on definition 7.39 Darboux sums and the definite integral ¶ ↺
-
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 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-9 ¶
-
depends_on
theorem 7.25
Heine–Cantor: uniform continuity
¶
- depends_on proposition 7.22 Sequential characterization ¶ ↺
- depends_on theorem 7.7 Bolzano–Weierstrass ¶ ↺
- proves proof ch:05-real-analysis@proof-10 ¶
- proves proof ch:05-real-analysis@proof-23 ¶
- depends_on theorem 7.25 Heine–Cantor: uniform continuity ¶ ↺
Supports
-
depends_on
lemma A.305
The chart integral is well defined
¶
-
depends_on
definition A.308
Integral over the manifold
¶
-
depends_on
theorem A.311
General Stokes theorem
¶
- depends_on corollary A.313 Stokes' theorem for an antisymmetric tensor field ¶
- depends_on lemma A.555 The actions are well defined ¶
- depends_on theorem 24.23 Poincaré–Cartan integral invariant ¶
-
depends_on
theorem A.311
General Stokes theorem
¶
-
depends_on
definition A.308
Integral over the manifold
¶
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 |
→ | Multiple integral | declared | appendices/A-long-proofs.tex:15017 |
depends_on |
→ | What the derivations below take as given | declared | appendices/A-long-proofs.tex:15017 |
depends_on |
← | The chart integral is well defined | declared | appendices/A-long-proofs.tex:15040 |