Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- For every set B, the empty set is the only map from the empty set to B, so the set of such maps is the singleton of the empty set.
Composite Maps into Classes, Images of Singletons, and Agreement of Maps by Induction
helperhlp:map-composites-singleton-images-agreement-2026aA map on a set may be formed from maps into classes by composing with a map on a product, the image of a singleton under a class is read off its pairs, and two maps agree on the elements of a class lying in the natural numbers with zero once agreement passes from 0 and from k to…- Two maps whose domains both contain u share a pair (u,v) with v a set exactly when their values at u agree.
The Graph of Multiplication on ℕ₀ Is Given by a Predicative Formula
helperhlp:omega-multiplication-predicative-2026aThe condition that a set is the triple ((m, n), m·n) for natural numbers m and n is expressed by a predicative formula, both with m and n as variables and with m and n bound by existential quantifiers.Predicative Formulas for Differences, Quotients, Absolute Values, Distances and the Strict Order of the Real Numbers, at Any Variable Positions
helperhlp:real-arithmetic-predicative-2026aMembership in the real numbers together with being the difference, quotient, absolute value or distance of given real numbers, and the strict order of the real numbers, are predicative conditions at any variable positions.- For pairwise distinct positions i, j, k, the condition that the set variable x_i is an injective map from x_j to x_k is expressed by a predicative formula.
Induction on ℕ₀ from 0 for a Condition Expressed by a Predicative Formula
lemmalem:omega-induction-predicative-2026aSet TheoryInduction from 0 on the natural numbers with zero for any condition expressed by a predicative formula, with the induction step stated either for the successor S(k) or for the sum n+1.The True Condition and Agreement of Two Classes at a Pair Are Predicative
helperhlp:predicative-true-pair-agreement-2026aThe condition that always holds is expressed by a predicative formula in any number of variables, and so is the condition that some set v makes the pair (x, v) an element of two given classes.Atomic Predicative Formulas: Equality with Unordered Pairs, Singletons and Successors
helperhlp:atomic-predicative-formulas-2026aSet TheoryThe formulas saying that a variable equals the unordered pair, the singleton or the successor of variables are predicative and mean what they say when the arguments are sets.- A finite sum of functions of class Cᵏ on an open subset of ℝⁿ is of class Cᵏ, and a finite sum of smooth functions is smooth.
Derivatives along Lines in ℝⁿ: the Line t ↦ x+th, and Partial Derivatives as Derivatives along Coordinate Axes
lemmalem:derivatives-along-lines-euclidean-2026aAnalysisThe line t ↦ x+th has derivative h at every point of an interval, and a partial derivative of a real function on an open subset of ℝⁿ is the same as the derivative of the function along the corresponding coordinate axis.The Line t ↦ x+th and Values of a Function along a Line in ℝⁿ, as Functions
helperhlp:euclidean-line-maps-2026aFor points x and h of ℝⁿ and a set J of reals, the line t ↦ x+th and the values t ↦ F(x+th) of a map F along it are maps on J.Lines, Scalar Multiples, Basis Directions, Small Balls and Matrix Rows in ℝⁿ
helperhlp:euclidean-vector-rules-2026aRules for points x + th on a line in ℝⁿ, for multiples of standard basis vectors, for small displacements inside an open set, and for a coordinate of a matrix-vector product as a dot product with a row.Order Rules for Products, Halves, Minima and Absolute Values in ℝ
helperhlp:real-order-rules-type-2026aThe ordered-field rules of lem:ordered-field-inequalities-nbg-2026c (products, halving, strict bounds on absolute values) read in the type Real, together with a positive number below two positives and the reciprocal, in the form the Lean formalization uses.Cᵏ Diffeomorphisms Between Open Subsets of ℝⁿ
definitiondef:ck-diffeomorphism-euclidean-2026aAnalysisA Cᵏ (respectively smooth) diffeomorphism of an open set W onto an open set V in ℝⁿ is an injective Cᵏ (respectively smooth) function from W onto V whose inverse is again Cᵏ (respectively smooth).- The standing setting for differential calculus on open subsets of ℝⁿ: the notation of functions of class Cᵏ, with the first-order, higher-order, inverse and implicit function, and differentiation-under-the-integral results as background.
- At a local extremum of a C¹ function restricted to the zero set of m C¹ constraints, the gradient of the function is a linear combination of the gradients of the constraints, provided some m columns of the constraints' Jacobian matrix form an invertible matrix; for one constraint…
- If F(a, b) = 0 for a function F of class Cᵏ of (x, y) ∈ ℝⁿ × ℝᵐ with values in ℝᵐ, and the derivative of F in y at (a, b) is invertible, then near (a, b) the equation F(x, y) = 0 has exactly one solution y = g(x), and g is of class Cᵏ with the derivative obtained by differentiati…
- Notation for functions of class Cᵏ and smooth functions on open subsets of Euclidean space, second partial derivatives, local extrema and pointwise operations on functions.
- There is exactly one sequence of sets of real-valued functions on U, indexed by k in ℕ₀, starting with the continuous functions and passing from k to k+1 by requiring that all first partial derivatives exist on U and lie in the k-th set.