Alphabeta MathArticle items · 04 — Every nonempty finite set of reals has a maximum and a minimum
Presents 28 items from the article and its immediate prerequisites, covering published library prerequisites.
1 · Prerequisites
- Maximum and minimum of a set
- The principle of mathematical induction
- Addition of natural numbers
- Complete ordered field (least-upper-bound property)
- Ordered field
- The indicator random variable of an event
- Expectation of a real random variable on a finite probability space
- Finite sums and finite products, by recursion
- The integers as equivalence classes of pairs of naturals
- The natural numbers ℕ (von Neumann)
- The naturals embed in the integers
- The integers embed in the rationals
- The rationals embed densely in the reals
- Discreteness: σ(n) is the immediate successor
- The integers form a totally ordered ring
- The integers form a commutative ring
- Every complete ordered field is Archimedean
- The well-ordering principle
- Canonical naturals are positive and strictly increasing
- Order is preserved by adding a constant and by adding inequalities
- Basic properties of the absolute value
- Dedekind-complete ordered real field
- Continuity and derivative on a real interval
- Rolle's theorem from attained extrema
- Real elementary functions and their domains
- Sum, product, quotient, and chain rules from difference quotients
- Power series may be differentiated term by term inside their radius
- Real and complex modulus product and triangle inequalities
- Elementary factorial and geometric series converge uniformly
- Real intervals, complex rectangles and ball enclosures
- Outward-rounded interval, rectangle and ball operations
- Directed dyadic rounding encloses with explicit underflow and overflow bounds
- The nonnegative Lebesgue integral
- The simple integral is monotone, homogeneous, and additive
- The integral of a nonnegative simple function
- The simple integral is independent of the chosen representation
- A Lipschitz self-map of ℝⁿ carries Lebesgue null sets to Lebesgue null sets
- A box with a degenerate side is Lebesgue null, and so is every coordinate hyperplane in ℝⁿ
- Lipschitz map, α-Hölder map for rational 0 < α ≤ 1, and contraction
- Every Euclidean linear map has a unique matrix and satisfies ‖Lh‖₂≤ K‖h‖₂ for some K≥0
- Assuming countable choice, L(ℝⁿ) is a sigma-algebra containing every elementary set and λₙ is a complete measure extending elementary volume
- The Euclidean inner product ⟨ x,y⟩ = ∑_k<n xₖ yₖ on ℝⁿ
- The orthogonal complement W^⊥={v:⟨ v,w⟩=0 for all w∈ W}
- In finite dimension, W^⊥⊥=W and dim W+dim W^⊥=dim V
- Linear subspace of a vector space
- Linear map between vector spaces over the same field
- ℝⁿ as the set of functions n → ℝ, and d₁, d₂, d_∞ are metrics on it
- The p-norms ‖ x‖ₚ for rational p ≥ 1, and ‖ x‖_∞
- Each ‖·‖ₚ is a norm on ℝⁿ, and the induced metrics are exactly d₁, d₂ and d_∞ of the published metric-spaces page
- Laws of finite sums and finite products
- The Axiom of Countable Choice (AC_ω)
- Continuity of f : A → ℝ at a point of A and on A: the ε-δ condition, its agreement with lim_x → c f(x) = f(c) at a limit point, and continuity at an isolated point
- Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero
- If lim_x → c f(x) = L ≠ 0 then |f| > |L|/2 on a punctured neighbourhood of c; in particular if L > 0 then f > L/2 > 0 there
- The ε-δ limit lim_x → c f(x) = L of f : A → ℝ at a limit point c of A
- Limit point, isolated point, adherent point, derived set, and dense subset of ℝ
- The ε-neighbourhood and the punctured ε-neighbourhood of a point of ℝ
- The reverse triangle inequality
- Integer powers aᵐ
- Field
- The derivative f'(c) = lim_x → c f(x) - f(c)/x - c of f : A → ℝ at a point c ∈ A that is a limit point of A, and differentiability on a set
- Carathéodory's characterisation: f is differentiable at c if and only if there is φ : A → ℝ, continuous at c, with f(x) - f(c) = φ(x)(x - c) for every x ∈ A, and then φ is unique and φ(c) = f'(c)
- A function differentiable at c is continuous at c
- A field has no zero divisors: ab = 0 ⟹ a = 0 or b = 0
- A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
- The Cauchy-Schwarz inequality for finite sums
- Minkowski's inequality for finite sums (rational exponent)
- Square roots exist: a unique √a ≥ 0 with (√a)² = a; the positives are {x² : x ≠ 0}
- Squaring is monotone on the nonnegatives
- Absolute value in an ordered field
- Real and complex inner product spaces, with the inner product linear in the first argument
- The norm ‖ v‖=√⟨ v,v⟩ induced by a real or complex inner product
- Conjugation is an involutive real-field automorphism, zz̄=|z|², and modulus is definite, multiplicative, and subadditive
- Existence and uniqueness of n-th roots: a unique a^1/n ≥ 0 with (a^1/n)ⁿ = a
- Linear independence: a finite list v : n → V is independent when ∑_i<n λᵢ vᵢ = 0_V forces every λᵢ = 0_F, and a subset S ⊆ V is independent when every injective finite list into S is independent
- The total (Fréchet) derivative Df(a) as the linear first-order approximation with o(‖h‖₂) remainder
- Total differentiability gives a local O(‖h‖₂) increment bound and therefore continuity
- A linear map L:ℝᵐ→ℝⁿ in Euclidean coordinates
- Law or distribution of a random element
- Expectation of a nonnegative or integrable random variable
- The law of a random element is a probability measure
- Composition with a Borel measurable outer map preserves measurability
- Every nonnegative measurable function is the increasing limit of simple measurable functions
- Monotone convergence for the integral
- Integrable real and complex functions, and their integrals
- The Lebesgue integral is linear on L¹(μ)
- Closure properties of measurable functions used by the integral
- Peano's mixed-partial theorem from continuity of one mixed partial
- Cᵏ maps and multi-index derivative notation in Euclidean space
- Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right
- A subspace is compact exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it
- Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison
- Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace
- Every natural-number-indexed list of nonempty sets has a choice function on its family of values
- Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space
- In an orthonormal basis, self-adjoint means conjugate-transpose symmetry and normal means commuting with the conjugate transpose
- The complex numbers are algebraically closed
- If the characteristic polynomial of an endomorphism splits, some orthonormal basis makes its matrix upper triangular
- A normal upper-triangular matrix is diagonal
- Connected components, quasicomponents, and totally disconnected spaces
- A union of connected subspaces with a point in common is connected, and so is a union of a family in which every member meets a fixed connected member
- If A is connected and A ⊆ B ⊆ Ā then B is connected; in particular the closure of a connected set is connected
- Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets
- Interior, closure, boundary, exterior, derived set and isolated point in a topological space
- The Borel sigma-algebra of a topological space
- Nonempty intersections of sigma-algebras are sigma-algebras, so the generated sigma-algebra exists and is minimal
- For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and f(Ā) ⊆ f(A)
- The real numbers ℝ as Dedekind cuts
- Order on the Dedekind reals
- Dedekind cut
- Inclusion totally orders the Dedekind reals
- The Dedekind reals form a totally ordered field
- An endomorphism is diagonalisable exactly when V=⨁_i<rE_λᵢ(T) for some finite list of distinct scalars λᵢ
- Algebraic multiplicity as the exponent of x-λ in χ_T, and geometric multiplicity as dim E_λ(T)
- Eigenvectors belonging to pairwise distinct eigenvalues are linearly independent
- Polynomials that split and splitting fields of a polynomial or a family of polynomials
- The basis-independent characteristic polynomial χ_T of an endomorphism of a finite-dimensional space, including χ_T=1 in dimension zero
- χ_A(x) is monic of degree n; for n≥1 its xⁿ⁻¹ coefficient is -tr(A) and its constant coefficient is (-1)ⁿ det(A), while χ_0×0=1
- The determinant of a triangular matrix is the product of its diagonal entries
- For every finite-dimensional space, σ_F(T) is exactly the set of roots in F of χ_T
- The addition formulas for sine and cosine
- Parity and the Pythagorean identity for sine and cosine
- Tangent, cotangent, secant, and cosecant on their exact natural domains
- The exponential series converges absolutely for every real argument
- Inside the common radius the product of two power-series sums is represented by the Cauchy product of their coefficients
- The binomial theorem in ℝ: (x+y)ⁿ = ∑_k<n+1 iotaC(n, k) xᵏ y^ n-k
- C(n, k) k! (n-k)! = n! for k ≤ n; hence C(n, k) k! = n^k̲, the quotient n!/(k!(n-k)!) is a natural number, and C(n, k) = C(n, n-k)
- The set [A]ᵏ of k-element subsets and the binomial coefficient C(n, k) := | [n]ᵏ|
- The factorial n! and the falling factorial n^k̲, defined by recursion in ℕ
- The canonical natural ι(n) = n · 1_F of a field
- The exponential function is smooth and (exp)'=exp
- The exponential is positive and satisfies exp(-x)=1/exp(x)
- The mean value theorem, as the case g(x) = x of Cauchy's: for f continuous on [a,b] with a < b and differentiable on (a,b) there is c ∈ (a,b) with f(b) - f(a) = f'(c)(b-a)
- The sum of a real power series is continuous at every point strictly inside its interval of convergence
- Local and strict local extrema for scalar fields on Euclidean open sets
- Fermat's interior extremum theorem: if f has a local extremum at a point c interior to its domain and is differentiable at c, then f'(c) = 0
- The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case
- Convex, strictly convex, concave, strictly concave, and midpoint-convex real functions on an interval
- Probability measures and probability spaces
- Measures are monotone
- Measures on sigma-algebras
- Sigma-algebras
2 · Logical flowchart
Arrows show item dependencies. A grouped prerequisite node points to items that use one or more of its members; their exact links are listed above.
3 · Items
LemmaLibrary prerequisite
Every nonempty finite set of reals has a maximum and a minimum
LemmaLibrary prerequisite
Indicators turn event probabilities, intersections, and finite counts into expectations and products
LemmaLibrary prerequisite
Integer part: for every real x there is exactly one integer m with m ≤ x < m + 1
LemmaLibrary prerequisite
Mean value theorem on a closed real interval
LemmaLibrary prerequisite
Range-reduced exponential, logarithm and arctangent series have certified tails
LemmaLibrary prerequisite
Finite real interval operations enclose their exact values
PropositionLibrary prerequisite
Monotonicity and nonnegative homogeneity of the nonnegative integral
PropositionLibrary prerequisite
The nonnegative integral agrees with the simple integral on simple functions
TheoremLibrary prerequisite
Every affine hyperplane of ℝⁿ, and hence every proper linear subspace, is Lebesgue null
TheoremLibrary prerequisite
Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function
TheoremLibrary prerequisite
Sums, scalar multiples, products and quotients: (f+g)'(c) = f'(c) + g'(c), (α f)'(c) = α f'(c), (fg)'(c) = f'(c)g(c) + f(c)g'(c), and (f/g)'(c) = (f'(c)g(c) - f(c)g'(c))/g(c)² when g(c) ≠ 0
TheoremLibrary prerequisite
Cauchy-Schwarz |⟨ x,y⟩| ≤ ‖ x‖₂‖ y‖₂ with its equality case, the triangle inequality for ‖·‖₂, the parallelogram law and polarisation
TheoremLibrary prerequisite
Cauchy–Schwarz: |⟨ u,v⟩|≤‖ u‖‖ v‖, with equality exactly for linearly dependent vectors
TheoremLibrary prerequisite
The chain rule for total derivatives: D(g∘ f)(a)=Dg(f(a))∘ Df(a)
TheoremLibrary prerequisite
Change of variables for expectation
TheoremLibrary prerequisite
Clairaut--Schwarz theorem for continuous second partial derivatives
TheoremLibrary prerequisite
A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact
TheoremLibrary prerequisite
Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely
TheoremLibrary prerequisite
The components of a space are its maximal connected subsets, they partition it, and each of them is closed
TheoremLibrary prerequisite
A continuous map has Borel preimages of Borel sets
TheoremLibrary prerequisite
Dedekind completeness: the least-upper-bound property
TheoremLibrary prerequisite
An endomorphism is diagonalisable if and only if its characteristic polynomial splits and every eigenvalue's geometric multiplicity equals its algebraic multiplicity
TheoremLibrary prerequisite
Double-angle and quadratic power-reduction identities
TheoremLibrary prerequisite
The exponential addition formula exp(x+y)=exp(x)exp(y)
TheoremLibrary prerequisite
The exponential function is strictly increasing
TheoremLibrary prerequisite
Fermat's theorem: an interior differentiable local extremum has zero gradient
TheoremLibrary prerequisite
Finite Jensen inequality for a convex function and nonnegative weights summing to one
TheoremLibrary prerequisite