Alphabeta MathArticle items · 03 — Partial order and partially ordered set
Presents 28 items from the article and its immediate prerequisites, covering published library prerequisites.
1 · Prerequisites
- Cosine has a smallest positive zero, lying strictly between zero and two
- Signs, monotonicity intervals, and ranges of sine and cosine
- The derivatives of sine and cosine are cosine and minus sine
- A function differentiable at c is continuous at c
- Quarter-turn values and shifts by pi/2 and pi
- Parity and the Pythagorean identity for sine and cosine
- Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on [a,b] takes every value between f(a) and f(b)
- Continuous inverse theorem: a continuous injective f on an interval I is a bijection onto the order-convex set f[I], and the inverse g : f[I] → I is continuous and strictly monotone in the same sense as f
- Measures on sigma-algebras
- Measure spaces
- Finite probability spaces, outcome weights, events, and event probabilities
- The product ∏_i ∈ I Aᵢ := { f : I → ⋃_i ∈ I Aᵢ ∣ f(i) ∈ Aᵢ for every i ∈ I }
- Finite sums and finite products, by recursion
- Measurable rectangles in a product of measurable spaces
- The sigma-algebra generated by a family of sets
- Nonempty intersections of sigma-algebras are sigma-algebras, so the generated sigma-algebra exists and is minimal
- A measurable function between measurable spaces
- The Borel sigma-algebra of a topological space
- Multi-indexed power series in ℂᵐ and their absolute convergence
- A real-analytic function on an open subset of ℝ is locally represented by a convergent real power series
- An absolutely convergent multi-indexed power series is holomorphic and differentiates termwise
- A real power series about a centre, its interval of convergence, and its radius in [0,+∞]
- The factorial n! and the falling factorial n^k̲, defined by recursion in ℕ
- Integer powers aᵐ
- The canonical natural ι(n) = n · 1_F of a field
- Canonical naturals are positive and strictly increasing
- Series, partial sums, convergence and the sum, divergence, and the tail series
- The natural logarithm as the inverse of the exponential function
- Riemannian metrics, symmetric cotangent-bundle connections, and covariant Hessians
- The differential of a smooth real-valued function
- The Axiom Schema of Separation: for each formula φ, ∀ p̄ ∀ x ∃ y ∀ z (z ∈ y ↔ (z ∈ x ∧ φ(z,p̄)))
- The union ⋃ x of a set, and the binary union a ∪ b := ⋃ {a,b}
- The Axiom of Extensionality: ∀ x ∀ y (∀ z (z ∈ x ↔ z ∈ y) → x = y)
- Subset x ⊆ y, proper subset x ⊊ y, and the separation notation { z ∈ x : φ(z) }
- The sine and cosine power series converge absolutely for every real argument
- The tangent bundle as a disjoint union
- Assuming countable choice, the tangent bundle has a canonical smooth 2n-manifold structure
- Smooth sections, local sections, and support
- The standard normal density has total mass one
- The indefinite integral of a nonnegative measurable function is a measure
- Law or distribution of a random element
- The law of a random element is a probability measure
- Continuous functions on Euclidean spaces are Borel measurable
- The Dirac set function at a point
- The Axiom of Choice
- A finite simple graph is a finite vertex set together with a set of two-element vertex subsets
- Walks, closed walks, trails, paths and cycles, with length equal to the number of traversed edges
- Connected graphs and connected components defined by the existence of vertex paths
- Adjacency, incidence, open and closed neighbourhoods, vertex degree, minimum degree and maximum degree
- The cardinality | A| of a finite set
- The reals form a totally ordered field
- The Axiom of Pairing: ∀ x ∀ y ∃ z ∀ t (t ∈ z ↔ (t = x ∨ t = y))
- Expectation of a real random variable on a finite probability space
- Square roots exist: a unique √a ≥ 0 with (√a)² = a; the positives are {x² : x ≠ 0}
- Bernoulli random variables and binomial random variables as sums of independent Bernoulli trials
- Independent random elements
- The expectation of an indicator is the probability of the event
- Expectation depends only on the almost-everywhere class
- The general rectangle criterion agrees with the published finite random-variable definition
- Linearity, monotonicity, and the modulus bound for expectation
- Variance and covariance identities for random variables
- Variance of a finite sum as the sum of all variances and covariances
- The set [A]ᵏ of k-element subsets and the binomial coefficient C(n, k) := | [n]ᵏ|
- Independent random elements have product joint law
- Picard-Lindelöf local existence and uniqueness for first-order systems
- Continuous dependence of ODE solutions on initial data and parameters
- Gronwall's integral inequality with variable and constant coefficients
- A first-order initial value problem is equivalent to its Volterra integral equation
- For a ≤ b and f : [a,b] → ℝᵐ integrable when a<b, ‖∫ₐᵇ f‖₂ ≤ ∫ₐᵇ ‖ f‖₂; for a<b, ‖ f‖₂ is integrable
- The Euclidean inverse function theorem
- ℝ and ℝⁿ for n ≥ 1 with the Euclidean metric are complete, componentwise from the Cauchy criterion in ℝ
- A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value
- Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous
- 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)
- C² inverses and scalar return roots
- Integer part: for every real x there is exactly one integer m with m ≤ x < m + 1
- The naturals embed in the integers
- Discreteness: σ(n) is the immediate successor
- The integers form a totally ordered ring
- Order is preserved by adding a constant and by adding inequalities
- Ordered field
- Expectation factors over a finite product of mutually independent random variables
- Markov's inequality on a finite probability space
- The exponential addition formula exp(x+y)=exp(x)exp(y)
- The exponential is positive and satisfies exp(-x)=1/exp(x)
- The exponential function is smooth and (exp)'=exp
- The exponential function is strictly increasing
- The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t
- The chain rule, in one line from Carathéodory: if g is differentiable at c and f is differentiable at g(c), then f ∘ g is differentiable at c with (f ∘ g)'(c) = f'(g(c)) g'(c)
- 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
- Continuity and derivative on a real interval
- Real and complex modulus product and triangle inequalities
- Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors
- Monotonicity of x ↦ xⁿ and of n ↦ aⁿ
- Multivariate normal law, including singular covariance
- Characteristic function of a multivariate normal law
- Characteristic functions under affine maps and independent sums
- Uniqueness of a law from its characteristic function
- Cramer wold device
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
DefinitionLibrary prerequisite
Partial order and partially ordered set
DefinitionLibrary prerequisite
Pi as twice the smallest positive zero of cosine
DefinitionLibrary prerequisite
Principal inverse sine and inverse cosine
DefinitionLibrary prerequisite
Probability measures and probability spaces
DefinitionLibrary prerequisite
The finite product of finite probability spaces
DefinitionLibrary prerequisite
The product sigma-algebra and its finite iterates
DefinitionLibrary prerequisite
Random elements and real random variables
DefinitionLibrary prerequisite
Real analytic germs in several variables
DefinitionLibrary prerequisite
The real exponential function and the number e by a power series
DefinitionLibrary prerequisite
Real powers for positive bases, with the zero-base positive-exponent convention
DefinitionLibrary prerequisite
The Riemannian gradient is the metric dual of the differential
DefinitionLibrary prerequisite
The difference a ∖ b, the symmetric difference a △ b, and the complement X ∖ a relative to a set X
DefinitionLibrary prerequisite
Sine and cosine defined by their real power series
DefinitionLibrary prerequisite
A smooth vector field is a smooth section of the tangent bundle
DefinitionLibrary prerequisite
Standard normal and normal laws
DefinitionLibrary prerequisite
Trees, forests, leaves and isolated vertices
DefinitionLibrary prerequisite
The uniform probability space on a nonempty finite set
DefinitionLibrary prerequisite
The unordered pair {x,y} and the singleton {x} = {x,x}
DefinitionLibrary prerequisite
Variance, standard deviation, and covariance on a finite probability space
LemmaLibrary prerequisite
A Bernoulli(p) variable has mean p and variance p(1-p); a binomial(n,p) variable has mean np and variance np(1-p)
LemmaLibrary prerequisite
The Binomial count has its usual probability mass function
LemmaLibrary prerequisite
C¹ Euclidean maximal flows, variational dependence and the finite C² upgrade
LemmaLibrary prerequisite
Ceilings give the least positive integer meeting a real threshold
LemmaLibrary prerequisite
Chernoff bound for independent bernoulli trials
LemmaLibrary prerequisite
Sum, product, quotient, and chain rules from difference quotients
LemmaLibrary prerequisite
Deleting any edge of a tree separates it into exactly two tree components
LemmaLibrary prerequisite
1+x≤exp(x) for every real x, hence (1-p)ᵐ≤exp(-mp)
LemmaLibrary prerequisite