How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
as the set of functions , and , , are metrics on it
Statement
Let with . A von Neumann natural is the set of its predecessors, (The natural numbers (von Neumann)), so it can be used directly as an index set. Define
and write for , . Two elements of are equal exactly when they agree at every , functions being equal when they have the same values. For put
All three are well defined: the finite sums are those of Finite sums and finite products, by recursion; the sum of squares is nonnegative (Laws of finite sums and finite products, Squares of nonzero elements are positive) so it has a unique nonnegative square root (Square roots exist: a unique with ; the positives are ); and is a nonempty finite subset of , because , so it has a maximum (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).
Then , and are metrics on (Metric space: iff , symmetry, and the triangle inequality; pseudometric and ultrametric).
Why . For the set has exactly one element, the empty function, and and are the empty sum and its root; but would be the maximum of the empty set, which does not exist. The hypothesis is therefore not decoration, and it is carried by every statement about in this library.
Facts & Assumptions
Given: A natural ; elements ; and the lists , for , so that . Write , and .
Laws of finite sums (Laws of finite sums and finite products, Finite sums and finite products, by recursion): additivity, scaling, monotonicity; a sum of nonnegative terms is nonnegative, every single term is at most the sum, and a sum of nonnegative terms that vanishes has every term .
Absolute value (Basic properties of the absolute value, Absolute value in an ordered field): ; if and only if ; ; and .
Two-term triangle inequality: (The triangle inequality).
Minkowski's inequality at the rational exponent (Minkowski's inequality for finite sums (rational exponent)): .
Cauchy-Schwarz in root form (The Cauchy-Schwarz inequality for finite sums): .
Square roots (Square roots exist: a unique with ; the positives are ): every has a unique with ; in particular if and only if .
Squares (Squares of nonzero elements are positive, Integer powers ): always, and only for ; and monotonicity of squaring on the nonnegatives, for (Squaring is monotone on the nonnegatives).
Maximum of a nonempty finite set of reals: it exists, it belongs to the set, and it is an upper bound of the set (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).
Order arithmetic in : inequalities may be added and a constant added to both sides, in the strict form of Order is preserved by adding a constant and by adding inequalities and, together with the case of equality settled by totality (Ordered field, Complete ordered field (least-upper-bound property)), in the nonstrict form used below.
Proof
Separation for : is a sum of nonnegative terms, so it vanishes exactly when every vanishes, that is exactly when for all , that is exactly when .
Separation for : vanishes exactly when ; is a sum of nonnegative terms, so exactly when for every , which happens exactly when every , that is exactly when .
Separation for : the maximum belongs to and bounds it above, so it is exactly when every , that is exactly when .
Symmetry for all three: and for every , so the three defining expressions are unchanged when and are exchanged.
Triangle inequality for : applying [L4] to the lists and gives .
Expanding with additivity and scaling: .
By [L5] and : , and , with .
Triangle inequality for : for each , because the two maxima bound their sets; so is an upper bound of , and the maximum of that set is one of its elements, whence .
Combining steps 1.6 and 1.7: .
Both and are nonnegative, and by step 2.1 the square of the first is at most the square of the second, so monotonicity of squaring on the nonnegatives gives .
Each of , , satisfies (M1) by steps 1.1, 1.2 and 1.3, satisfies (M2) by step 1.4, and satisfies (M3) by steps 1.5, 3.1 and 1.8 respectively; hence all three are metrics on .
Remarks
- is defined ZFC-natively here, as the set of functions from the von Neumann natural to , precisely so that its coordinates are indexed by and the finite-sum machinery of Finite sums and finite products, by recursion, Minkowski's inequality for finite sums (rational exponent) and The Cauchy-Schwarz inequality for finite sums, all of which sum over , applies without any reindexing.
- No rational power appears anywhere above. The triangle inequality for is obtained from Cauchy-Schwarz and the existence of square roots, not from Minkowski at , so this lemma does not depend on the theory of rational exponents. Minkowski is used only at , where its statement is the termwise sum of the two-term triangle inequality.
- The three metrics are Lipschitz equivalent, with explicit constants, and in particular have the same topology; that computation is on the companion page and is not needed here.
Depends on
- Metric space: $d(x,y) = 0$ iff $x = y$, symmetry, and the triangle inequality; pseudometric and ultrametric
- The natural numbers $\mathbb{N}$ (von Neumann)
- Finite sums and finite products, by recursion
- Minkowski's inequality for finite sums (rational exponent)
- The Cauchy-Schwarz inequality for finite sums
- Every nonempty finite set of reals has a maximum and a minimum
- Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$; the positives are $\{x^2 : x \neq 0\}$
- Basic properties of the absolute value
- Laws of finite sums and finite products
- Maximum and minimum of a set
- Squaring is monotone on the nonnegatives
- Squares of nonzero elements are positive
- The triangle inequality
- Absolute value in an ordered field
- Integer powers $a^m$
- Ordered field
- Complete ordered field (least-upper-bound property)
- Order is preserved by adding a constant and by adding inequalities
Used by
- A Lebesgue measurable subgroup of (ℝⁿ,+) of positive measure is all of ℝⁿ Corollary
- A subset of ℝⁿ with the product topology is compact exactly when it is closed and bounded, the product topology being the Euclidean metric topology Corollary
- Assuming countable choice and dependent choice, a measurable function on a finite-measure subset of Rⁿ agrees there, off a small set, with a continuous function on Rⁿ Corollary
- At m=1, cube-nullity and cube-content-zero are exactly the published interval-cover notions Corollary
- At m=1, nondegenerate multidimensional rectangles, grid sums and the integral are exactly the published one-dimensional notions Corollary
- For n ≥ 1 every bounded sequence in ℝⁿ has a convergent subsequence Corollary
- If f : [a,b] → ℝᵐ is differentiable with integrable f' then ∫ₐᵇ f' = f(b)-f(a); and a bounded derivative makes f Lipschitz Corollary
- A curl-free C¹ field on the complement of a line that is not conservative Counterexample
- g(x,y) = xy/(x²+y²), extended by g(0,0)=0, is continuous in each variable separately and not continuous at the origin Counterexample
- The comb space is path-connected and fails to be locally connected at every point of the limit tooth strictly above the base, so path-connectedness does not imply local connectedness Counterexample
- Axis-parallel rectangles in ℝᵐ and their volume Definition
- Euclidean spheres and closed balls as subspaces of ℝⁿ Definition
- Half-open boxes in ℝⁿ and their volume Definition
- Jordan inner and outer content and Jordan measurable bounded sets in ℝᵐ Definition
- Local Lipschitz continuity in the state variable, locally uniform in time and parameters Definition
- Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space Definition
- Oscillation of a real function on subsets of ℝᵐ and at a point Definition
- Polygonal arcs and polygons as non-self-intersecting finite unions of line segments in ℝ² Definition
- Regions of the complement of a planar set and their frontiers Definition
- Series of vectors in ℝⁿ, absolute convergence, rearrangement, and the set of rearrangement sums Definition
- Simple polygonal regions, diagonals, and triangulations Definition
- The Euclidean inner product ⟨ x,y⟩ = ∑_k<n xₖ yₖ on ℝⁿ Definition
- The p-norms ‖ x‖ₚ for rational p ≥ 1, and ‖ x‖_∞ Definition
- Upper and lower semicontinuity on subsets of ℝⁿ Definition
- Vector-valued functions f : A → ℝᵐ, their limits and continuity, with the dictionary to the metric notions Definition
- A Euclidean right triangle has minsize proportional to its scale Example
- An additive f : ℝ → ℝ that is not x ↦ cx: the coefficient of one fixed Hamel basis vector. It is unbounded above and below on every nondegenerate interval, its graph is dense in ℝ², and every nonempty level set is dense in ℝ Example
- An open Euclidean unit ball is metrically incomplete Example
- Continuous kernel integral operator is compact on c of an interval Example
- Euclidean borel spaces are standard borel Example
- Every convex subset of ℝⁿ, in particular every ball and ℝⁿ itself, is path-connected and hence connected Example
- Horizontal translations of Z on the Euclidean plane are proper but not cobounded Example
- ℝ^* is homeomorphic to the unit circle by inverse stereographic projection, and ℕ^* is the ordinal space ω + 1 Example
- ℝⁿ as the product of n copies of the real line: the product topology is the Euclidean topology and the projections are continuous, open and surjective Example
- Scaling distinguishes sublinear minsize from a fixed perimeter cutoff Example
- The Cayley graph of ℤⁿ for the standard basis is the integer lattice, and its word metric is the sum of coordinate differences Example
- The cube [-M,M]ⁿ in ℝⁿ is totally bounded, with an explicit finite ε-net of grid points and no appeal to the integer part Example
- The inverse-square field is divergence free, and its flux through the sphere bounding the translated unit ball vanishes Example
- The map (x,z) ↦ x · z on ℝ × ℝ and its transpose z ↦ (x ↦ x · z) traced through the exponential law Example
- The metrics d₁, d₂ and d_∞ on ℝⁿ are metrics and are Lipschitz equivalent, with explicit constants Example
…and 35 more results.
Dependency tree · two levels
52 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Euclidean space (Wikipedia) (standard reference, not scraped)
- Taxicab geometry (Wikipedia) (standard reference, not scraped)
- Lp space (Wikipedia) (standard reference, not scraped)
- W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 2 (standard reference, not scraped)
- R. Gardner, Introduction to Topology, notes on Munkres Section 20: The Metric Topology (East Tennessee State University) (standard reference, not scraped)