Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
A Map into a Euclidean Space is Differentiable at Every Point
corollarycor:c1-vector-differentiable-2026aAnalysisMultivariable CalculusLet and be natural numbers, let be an open subset of Euclidean space , let with coordinate functions , and let . Suppose that is of class on , in the sense of clause 1 of…Chain Rule for Differentiable Functions Between Euclidean Spaces
theoremthm:chain-rule-differentiable-euclidean-2026bAnalysisMultivariable CalculusThe derivative matrix of a composite of differentiable functions between open subsets of Euclidean spaces is the product of the derivative matrices; the same holds for a real-valued outer function in gradient form, and along a differentiable curve.Linearity, Compatibility with the Matrix Product, and a Norm Bound for the Matrix-Vector Product
lemmalem:matrix-vector-product-properties-2026aAnalysisLinear AlgebraMultivariable CalculusLet , and be natural numbers and let be the real numbers, an ordered field with additive identity and order ; write for the absolute value of . Let be a real matrix with rows and columns, its entry in row and…Jacobian Matrix of a Local Smooth Extension on an Admissible Domain
lemmalem:smooth-extension-jacobian-2026aMultivariable CalculusLet and be natural numbers, let be an admissible domain in Euclidean space in the sense of Continuous n-Form, Support, and Zero Extension on a Euclidean or Half-Space Domain, and let . For a map into and…- If f is differentiable at x and g is differentiable at f(x), then g composed with f is differentiable at x with derivative g'(f(x)) f'(x).
The Derivative Is the Jacobian Matrix, and Is Unique
lemmalem:differentiable-derivative-matrix-2026bAnalysisMultivariable CalculusA gradient of a differentiable real-valued function is the vector of its partial derivatives, and a derivative matrix of a differentiable vector-valued function is its Jacobian matrix; both are unique, and differentiability can be checked componentwise.Differentiability at a Point for Functions Between Euclidean Spaces
definitiondef:differentiable-map-euclidean-2026bAnalysisMultivariable CalculusA function on an open subset of R^n is differentiable at a point with derivative matrix A (vector-valued) or with gradient p (real-valued) if the linear approximation error is at most epsilon times the norm of the increment for small increments.Jacobian Matrix of a Function Between Euclidean Spaces
definitiondef:jacobian-matrix-euclidean-2026bAnalysisMultivariable CalculusThe Jacobian matrix of a function from an open subset of R^n to R^m at a point is the m x n matrix of the partial derivatives of its component functions.- Let and be natural numbers and let be the real numbers. Identify the Cartesian product of Euclidean spaces with by writing a pair , with and …
Uniqueness of the Partial Derivative on an Open Subset of
lemmalem:partial-derivative-unique-euclidean-2026bMultivariable CalculusAt most one real number satisfies the difference-quotient condition defining the partial derivative of a real-valued function in a coordinate direction at a point.Derivatives of a Function Along a Line Segment in ℝⁿ
lemmalem:segment-derivative-c1-2026bMultivariable CalculusFor a function on an open subset of ℝⁿ restricted to a line t ↦ x + th, the first derivative is the gradient paired with h and, for a function of class C², the second derivative is the Hessian quadratic form in h; it also gives room around a segment and continuity along it.Functions of Class Cᵏ on an Open Subset of ℝⁿ
definitiondef:ck-map-euclidean-2026bMultivariable CalculusFor k in ℕ₀, the set 𝒞ᵏ(U) is the k-th member of the recursively defined family of classes; a real-valued function is of class Cᵏ on U if it lies in 𝒞ᵏ(U), and a vector-valued function if all its components do.Partial Derivative of a Real-Valued Function on an Open Subset of
definitiondef:partial-derivative-euclidean-2026bMultivariable CalculusDefines the partial derivative of a real-valued function on an open subset of R^n with respect to the i-th variable at a point, its notation, and the partial derivative function.- The real numbers are a Dedekind complete ordered field, denoted , with order relation . We use the following notation on . Let . 1. (Arithmetic notation) and denote the additive and multiplicative identity elements of…
Derivatives of Constants, the Identity, Sums, Scalar Multiples, Products, Reciprocals, Quotients and Powers
lemmalem:derivative-arithmetic-1d-2026bAt a point of an interval with at least two points: constants have derivative 0, the identity 1, and sums, scalar multiples, products, reciprocals, quotients and the powers t^(n+1) are differentiable with the usual formulas.Derivative and Continuity of the Scaled Exponential Function
lemmalem:scaled-exponential-derivative-metric-2026aLet be the real numbers, let be the real line, let be the exponential function, let , and define by The set is an interval, an…The Increment Form of the Derivative, and Differentiability Implies Continuity
lemmalem:differentiable-implies-continuous-1d-2026bA real number is a derivative of f at x exactly when f(t) - f(x) = phi(t)(t - x) for a map phi continuous at x with phi(x) equal to that number; hence a function differentiable at a point is continuous there.Fundamental Theorem of Calculus, Part II: Evaluating an Integral by an Antiderivative
theoremthm:ftc-part2-2026aIf f is integrable on [a,b] and F is continuous on [a,b] with F' = f on (a,b), then the integral of f over [a,b] equals F(b) - F(a).Fundamental Theorem of Calculus, Part I: the Indefinite Integral is Lipschitz, Continuous, and Differentiable at Points of Continuity
theoremthm:ftc-part1-2026aFor a bounded integrable f on [a,b], the indefinite integral F(x) = integral of f from a to x is Lipschitz with constant any bound of |f|, hence continuous, and F'(x0) = f(x0) wherever f is continuous.A Continuous Function with Vanishing Derivative is Constant
corollarycor:vanishing-derivative-constant-2026aLet be real numbers with in the order of the ordered field , let be the closed interval determined by and , regarded as a subset of the real line , and let the codomain carry the same metric…