theorem 7.7 Bolzano–Weierstrass

open in the book · parts/02-mathematical-methods/05-real-analysis.tex:111 · p. 204

Rests on

depends_on corollary A.45 Archimedean property and density of $\Q$ ¶
- depends_on definition A.36 Cut ¶
- depends_on theorem A.40 Least-upper-bound property ¶
  - depends_on definition A.36 Cut ¶ ↺
  - depends_on definition A.38 Order on $\R$ ¶
    - depends_on definition A.36 Cut ¶ ↺
  - proves proof app:A-long-proofs@proof-29 ¶
- proves proof app:A-long-proofs@proof-32 ¶
depends_on corollary A.46 Monotone convergence ¶
- depends_on theorem A.40 Least-upper-bound property ¶ ↺
- proves proof app:A-long-proofs@proof-33 ¶
proves proof ch:05-real-analysis@proof-4 ¶

Supports

depends_on lemma A.454 Arzelà–Ascoli on an interval ¶
- depends_on theorem A.490 Equicontinuity of the normalised class ¶
- depends_on theorem A.470 $T$ is compact ¶
  - depends_on theorem A.471 Spectral decomposition and completeness in $L^{2}_{r}$ ¶
    - depends_on lemma A.472 The pairing identity ¶
- depends_on theorem A.455 Compact embedding of $W^{1,r}(a,b)$ into the continuous functions ¶
  - depends_on theorem A.456 Convexity in $q$ implies weak lower semicontinuity ¶
depends_on theorem 7.24 Extreme value theorem ¶
- depends_on lemma A.221 Counting identity ¶
- depends_on lemma 6.19 Continuous argument along a path ¶
  - depends_on definition 6.20 Winding number ¶
    - depends_on example 6.21 ex:top-winding-values ¶
    - depends_on lemma 6.22 Nearby loops wind alike ¶
      - depends_on proposition 6.23 The punctured plane is not simply connected ¶
  - depends_on lemma 6.22 Nearby loops wind alike ¶ ↺
- depends_on theorem 7.40 Continuous functions are integrable ¶
  - depends_on corollary A.502 All iterated orders agree ¶
    - depends_on lemma A.507 Coordinate permutations ¶
  - depends_on definition 16.11 Admissible class; functional ¶
    - depends_on definition 16.59 Weierstrass excess function ¶
    - depends_on definition 16.12 The two norms; weak and strong neighbourhoods ¶
      - depends_on definition 16.13 Weak and strong extrema ¶
    - depends_on definition 16.15 Variation; the first variation ¶
      - depends_on definition 16.83 One-parameter transformation group; variational symmetry ¶
      - depends_on lemma 16.18 Fundamental lemma ¶
      - depends_on proposition 16.16 Stationarity is necessary ¶
      - depends_on theorem 16.43 Euler's rule for integral constraints ¶
    - depends_on proposition 16.68 Weierstrass' counterexample ¶
  - depends_on definition 9.137 Elliptic integrals of the three kinds ¶
    - depends_on definition 9.140 Amplitude and the Jacobi elliptic functions ¶
      - depends_on proposition 9.143 A cubic quadrature between two turning points ¶
      - depends_on proposition 9.141 First properties ¶
      - depends_on proposition 9.144 The pendulum equation at finite amplitude ¶
    - depends_on proposition 9.139 Series for the complete integral of the first kind ¶
      - depends_on proposition 9.144 The pendulum equation at finite amplitude ¶ ↺
  - depends_on lemma A.501 Iterated integration over a box ¶
    - depends_on corollary A.502 All iterated orders agree ¶ ↺
    - depends_on lemma A.509 Primitive maps have the substitution property ¶
      - depends_on proposition A.511 The substitution property is universal ¶
  - depends_on lemma 16.18 Fundamental lemma ¶ ↺
  - depends_on remark 7.128 What the derivations below take as given ¶
    - depends_on lemma A.312 The computation in one chart ¶
    - depends_on theorem 7.129 Change of variables in a multiple integral ¶
      - depends_on example 7.130 The two Jacobians this treatise uses ¶
      - depends_on lemma A.518 The excised ball ¶
      - depends_on proposition A.519 The convolution exists ¶
    - depends_on theorem 7.133 Gauss ¶
      - depends_on lemma A.708 The disturbance flux vanishes ¶
      - depends_on lemma A.712 The force is a far-field integral ¶
      - depends_on lemma A.117 Laplacian in orthogonal coordinates ¶
      - depends_on lemma 44.10 Divergence theorem on $(M,g)$ ¶
      - depends_on lemma 31.11 Transport theorem for a material volume ¶
      - depends_on lemma 106.86 A shift of a divergent integral leaves a surface term ¶
      - depends_on lemma 10.44 Green's identities ¶
      - depends_on lemma 10.58 Darboux's equation for spherical means ¶
      - depends_on proposition 23.54 The geometrical amplitude diverges ¶
      - depends_on proposition 10.57 Energy in a backward cone ¶
      - depends_on theorem 16.36 Euler–Lagrange equations for several independent variables ¶
      - depends_on theorem 32.6 Evolution of phase volume ¶
      - … 1 more
    - depends_on theorem 7.131 Green ¶
      - depends_on proposition 32.33 Bendixson's negative criterion ¶
      - depends_on proposition 9.36 Bendixson–Dulac negative criterion ¶
      - depends_on theorem 7.132 Stokes ¶
      - depends_on theorem 8.12 Cauchy ¶
      - depends_on theorem 13.41 Holonomy equals the enclosed curvature; local Gauss–Bonnet ¶
      - depends_on theorem 10.96 Rankine–Hugoniot condition ¶
    - depends_on theorem A.303 Change of variables for multiple integrals; quoted ¶
      - depends_on lemma A.305 The chart integral is well defined ¶
  - depends_on theorem 7.42 Fundamental theorem of calculus, I ¶
    - depends_on corollary 7.110 Variable limits of integration ¶
    - depends_on definition A.450 The space $W^{1,r}(a,b)$ ¶
      - depends_on definition A.462 The weighted space and the energy space ¶
      - depends_on lemma A.453 Uniform bound and uniform Hölder continuity ¶
      - depends_on lemma A.452 Young and Hölder ¶
    - depends_on lemma A.520 A $C^{1}$ limit ¶
      - depends_on proposition A.521 Every derivative passes onto $g$ ¶
    - depends_on lemma A.440 Grönwall's inequality ¶
      - depends_on theorem A.441 Continuous dependence on the data and on the initial point ¶
    - depends_on lemma 16.19 du Bois-Reymond ¶
      - depends_on lemma 16.20 Mixed form ¶
    - depends_on lemma 9.10 Grönwall's inequality ¶
      - depends_on proposition 9.11 Continuous dependence on the initial data ¶
      - depends_on proposition 9.31 Lyapunov's first method: asymptotic stability ¶
    - depends_on proposition 11.22 Properties of the distribution function ¶
      - depends_on proposition 11.27 Probability integral transform ¶
    - depends_on proposition 9.18 The linear equation: integrating factor ¶
      - depends_on proposition 9.87 The distinguished limit, and which end carries the layer ¶
    - depends_on proposition 9.19 Separation of variables ¶
    - depends_on theorem 7.43 Fundamental theorem of calculus, II ¶
      - depends_on corollary 7.44 Substitution and integration by parts ¶
      - depends_on corollary 16.23 du Bois-Reymond form ¶
      - depends_on lemma 7.116 Functions vanishing on a regular zero set ¶
      - depends_on lemma A.72 Iterated integral inequality ¶
      - depends_on lemma A.520 A $C^{1}$ limit ¶ ↺
      - depends_on lemma A.172 Dirichlet ¶
      - depends_on lemma A.221 Counting identity ¶ ↺
      - depends_on lemma A.312 The computation in one chart ¶ ↺
      - depends_on proposition 7.85 Irrationality of $\pi$ ¶
      - depends_on proposition 8.10 Fundamental theorem for contours ¶
      - depends_on proposition 17.41 The identities physics uses ¶
      - depends_on proposition 17.73 Initial- and final-value theorems ¶
      - … 4 more
    - depends_on theorem 10.52 Duhamel's principle ¶
      - depends_on corollary 10.53 Duhamel for the wave equation ¶
- depends_on theorem 7.42 Fundamental theorem of calculus, I ¶ ↺
- depends_on theorem 7.34 Rolle ¶
  - depends_on theorem 7.37 Cauchy mean value theorem and l'Hôpital's rule ¶
    - depends_on lemma A.306 The standard smooth bump ¶
      - depends_on lemma A.307 Partition of unity on a compact manifold ¶
  - depends_on theorem 7.35 Mean value theorem ¶
    - depends_on corollary 7.36 cor:ana-mvt-consequences ¶
      - depends_on definition 7.41 Antiderivative ¶
      - depends_on lemma 7.67 The limit over real exponents ¶
      - depends_on lemma 7.75 The first quadrant ¶
      - depends_on lemma 7.78 Chord, arc, tangent ¶
      - depends_on lemma 9.10 Grönwall's inequality ¶ ↺
      - depends_on proposition 7.108 Euler's theorem on homogeneous functions ¶
      - depends_on proposition 7.61 The logarithm ¶
      - depends_on proposition 9.19 Separation of variables ¶ ↺
      - depends_on theorem 7.115 Constant rank ¶
    - depends_on lemma 7.93 A polynomial has at most $n$ roots ¶
    - depends_on lemma A.500 Graphs and $C^{1}$ images have zero content ¶
      - depends_on corollary A.514 Degeneracy on a negligible set ¶
      - depends_on lemma A.512 The boundary strip is thin ¶
    - depends_on lemma A.73 Differentiation under the integral sign ¶
      - depends_on lemma A.77 Poincaré lemma, converse form ¶
    - depends_on lemma A.287 The Newton map contracts ¶
      - depends_on lemma A.288 The iteration converges ¶
    - depends_on lemma A.290 $h$ is Lipschitz ¶
      - depends_on lemma A.291 $h$ is differentiable, with the stated derivative ¶
    - depends_on lemma A.440 Grönwall's inequality ¶ ↺
    - depends_on lemma A.226 The level factor ¶
    - depends_on lemma A.468 The kernel is well defined, symmetric and Lipschitz ¶
      - depends_on theorem A.470 $T$ is compact ¶ ↺
    - depends_on lemma 11.68 Jensen's inequality for the logarithm ¶
    - depends_on proposition 7.105 Clairaut–Schwarz ¶
      - depends_on definition 10.4 The second-order operator ¶
      - depends_on lemma A.75 Differentiating a pullback along a flow ¶
      - depends_on lemma 22.20 The symplectic condition ¶
      - depends_on proposition 7.123 Second-order identities of the nabla calculus ¶
      - depends_on proposition 30.25 Twenty-one constants ¶
      - depends_on proposition 30.14 Saint-Venant compatibility is necessary ¶
      - depends_on proposition 22.30 Properties of the Poisson bracket ¶
      - depends_on proposition 13.148 prop:mfd-torsion-tensor ¶
      - depends_on proposition 10.16 Cauchy's characteristic strips ¶
      - depends_on theorem 7.132 Stokes ¶ ↺
      - depends_on theorem 7.106 Taylor's theorem in several variables ¶
      - depends_on theorem 13.152 Riemann tensor; Ricci identity with torsion ¶
      - … 2 more
    - depends_on theorem 7.100 $C^{1}$ implies differentiable ¶
      - depends_on lemma A.291 $h$ is differentiable, with the stated derivative ¶ ↺
      - depends_on remark 7.101 Partial derivatives alone do not suffice ¶
      - depends_on theorem 7.112 Implicit function theorem ¶
      - depends_on theorem A.286 Implicit function theorem ¶
    - … 2 more
  - depends_on theorem 7.38 Taylor's theorem with Lagrange remainder ¶
    - depends_on definition 32.57 The Hénon–Heiles Hamiltonian ¶
    - depends_on definition 32.12 Linearization ¶
      - depends_on proposition 32.17 Classification of planar fixed points ¶
      - depends_on theorem 32.15 Hartman–Grobman, restated from Part II ¶
      - depends_on theorem 32.13 Linear stability ¶
    - depends_on lemma A.754 Exact depth expansion ¶
      - depends_on proposition A.755 The Boussinesq pair ¶
    - depends_on lemma A.187 Exponentiation ¶
    - depends_on lemma A.138 The flat exponential ¶
      - depends_on definition A.139 The standard radial mollifier ¶
      - depends_on lemma A.140 Properties of the mollifier ¶
    - depends_on lemma A.452 Young and Hölder ¶ ↺
    - depends_on lemma A.212 Second-order flatness ¶
      - depends_on lemma A.213 The three minima ¶
    - depends_on lemma A.209 Uniform third-order remainder ¶
      - depends_on corollary A.210 Uniform quadratic approximation on the $n^{-1/2}$ scale ¶
      - depends_on lemma A.211 Root-$n$ localisation ¶
    - depends_on phenomenon 28.13 Universality of small oscillations ¶
    - depends_on proposition 16.50 The second variation ¶
    - depends_on proposition 17.67 Holomorphy ¶
      - depends_on theorem 17.78 Causality implies dispersion relations ¶
      - depends_on theorem 17.93 Fundamental strip and holomorphy ¶
    - depends_on proposition 9.88 The model problem, and the error of the composite ¶
    - … 2 more
depends_on theorem 7.25 Heine–Cantor: uniform continuity ¶
- depends_on lemma A.195 Riemann–Lebesgue, continuous compactly supported case ¶
  - depends_on lemma A.196 Inversion for a difference ¶
    - depends_on theorem A.198 Esseen's smoothing inequality ¶
- depends_on lemma A.500 Graphs and $C^{1}$ images have zero content ¶ ↺
- depends_on lemma A.499 What zero content buys ¶
  - depends_on corollary A.514 Degeneracy on a negligible set ¶ ↺
  - depends_on lemma A.500 Graphs and $C^{1}$ images have zero content ¶ ↺
  - 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 ¶
- depends_on lemma A.512 The boundary strip is thin ¶ ↺
- depends_on lemma A.73 Differentiation under the integral sign ¶ ↺
- depends_on lemma A.176 Helly–Bray ¶
  - depends_on corollary A.181 The converse ¶
- depends_on lemma A.488 Small chords cut off small arcs ¶
  - depends_on theorem A.490 Equicontinuity of the normalised class ¶ ↺
- depends_on lemma 14.34 The $n$-sphere is simply connected for $n \ge 2$ ¶
- depends_on lemma 6.19 Continuous argument along a path ¶ ↺
- depends_on remark 7.128 What the derivations below take as given ¶ ↺
- depends_on theorem 7.40 Continuous functions are integrable ¶ ↺
- depends_on theorem 7.109 Leibniz integral rule ¶
  - depends_on corollary 7.110 Variable limits of integration ¶ ↺
  - depends_on lemma 7.116 Functions vanishing on a regular zero set ¶ ↺
  - depends_on lemma A.607 A zero-free entire function is an exponential ¶
    - depends_on proposition A.609 The exponent is a quadratic polynomial ¶
      - depends_on proposition A.611 The constraint on $\Gamma$ ¶
  - depends_on lemma A.599 One variable, complex coefficient ¶
    - depends_on lemma A.601 Several variables, complex symmetric matrix ¶
      - depends_on proposition A.612 The dictionary between $A$ and $\Gamma$ ¶
      - depends_on proposition A.602 The Wigner function of a Gaussian is a positive Gaussian ¶
  - depends_on proposition A.524 Rate of decay ¶
  - depends_on proposition A.521 Every derivative passes onto $g$ ¶ ↺
  - depends_on theorem 7.137 Helmholtz decomposition ¶
    - depends_on remark A.527 The hypotheses, and what happens without them ¶
    - depends_on remark 30.46 Why the plane-wave route, and not the potentials ¶
    - depends_on remark 30.27 Two results this chapter borrows from Part II ¶
    - depends_on remark 10.73 What compact support is doing, and the rate that replaces it ¶
    - depends_on remark 10.74 Where the decomposition is used, and what it costs ¶
- … 1 more
depends_on theorem A.173 Helly's selection theorem ¶
- depends_on lemma A.176 Helly–Bray ¶ ↺
- depends_on lemma A.175 Tightness makes the Helly limit proper ¶

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`	→	Archimedean property and density of $\Q$	declared	parts/02-mathematical-methods/05-real-analysis.tex:113
`depends_on`	→	Monotone convergence	declared	parts/02-mathematical-methods/05-real-analysis.tex:113
`depends_on`	←	Arzelà–Ascoli on an interval	declared	appendices/A-long-proofs.tex:22311
`depends_on`	←	Extreme value theorem	declared	parts/02-mathematical-methods/05-real-analysis.tex:394
`depends_on`	←	Heine–Cantor: uniform continuity	declared	parts/02-mathematical-methods/05-real-analysis.tex:414
`depends_on`	←	Helly's selection theorem	declared	appendices/A-long-proofs.tex:9038
`proves`	←	ch:05-real-analysis@proof-4	declared	parts/02-mathematical-methods/05-real-analysis.tex:116