Theorems

A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.

Showing 961-980 of 1428

Back Next

A Finite Sum of Vectors with Vanishing Tail
lemmalem:finite-sum-vanishing-tail-2026aAlgebra Linear Algebra
Let $K$ be a field, let $V$ be a vector space over $K$ with zero vector $0_{V}$ , let $n$ be a natural number, let $[n]$ be the initial segment it determines, and let $<$ be the strict order on $\mathbb{N}$ . Let $u\in V^{n}$ be an $n$ -tuple in $V$ and let $j\in[n]$ be such that…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-04T00:53:36.760059Z
Any Two Orthonormal Bases of a Complex Inner Product Space Have the Same Size
theoremthm:orthonormal-basis-size-invariance-2026aAnalysis Linear Algebra
Let $V$ together with $\langle\cdot,\cdot\rangle$ be a complex inner product space, let $m$ and $n$ be natural numbers, and let $e\in V^{n}$ and $f\in V^{m}$ be tuples in $V$ that are both orthonormal bases of $V$ . Then $m=n$ .
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-04T00:21:01.628988Z
Interchange of a Finite Double Sum
lemmalem:finite-double-sum-interchange-2026aAlgebra
Let $K$ be a field, let $m,n$ be natural numbers, and let $[m]$ and $[n]$ be the initial segments they determine. Let $a\in(K^{n})^{m}$ be an $m$ -tuple of $n$ -tuples in $K$ , with components $(a_{j})_{k}$ for $j\in[m]$ and $k\in[n]$ , and let $b\in K^{m}$ and $c\in K^{n}$ be given…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-04T00:17:40.814743Z
The Sum of $n$ Ones is Strictly Increasing in $n$
lemmalem:sum-of-ones-strictly-increasing-2026aAnalysis Algebra
Let $\mathbb{N}$ be the set of natural numbers, with successor map $S$ and order relations $<$ and $\le$ , and for $n\in\mathbb{N}$ let $[n]$ be the initial segment it determines. Let $\mathbb{R}$ be the ordered field of real numbers, with additive identity $0$ and multiplicative…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-04T00:17:33.383707Z
Tuples in a Set
definitiondef:finite-tuple-power-2026aAlgebra Set Theory
Let $X$ be a set, let $n$ be a natural number, and let $[n]$ be the initial segment determined by $n$ , that is, the set of natural numbers $k$ with $1\le k\le n$ . The set $X^{n}$ is the set of all maps from $[n]$ to $X$ . An element $x\in X^{n}$ is called an $n$ -tuple in $X$ ; for…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T01:10:15.970956Z
Dropping a Redundant Vector from a Spanning Family
lemmalem:span-drop-redundant-vector-2026bAlgebra Linear Algebra
Let $K$ be a field, let $V$ be a vector space over $K$ , and let $n$ be a natural number. Inequalities between natural numbers use the order relations on $\mathbb{N}$ . Let $v$ be a tuple in $V^{n+1}$ that spans $V$ , let $j$ be a natural number with $j\le n+1$ , and let $v^{(j)}$ b…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:48:15.998758Z
Extraction of a Summand from a Finite Sum of Vectors
lemmalem:finite-sum-extraction-2026aAlgebra Linear Algebra
Let $K$ be a field, let $V$ be a vector space over $K$ , and let $n$ be a natural number. Inequalities between natural numbers use the order relations on $\mathbb{N}$ . Let $b$ be a tuple in $V^{n+1}$ , with components $b_{k}$ for $1\le k\le n+1$ , and let $j$ be a natural number wi…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:48:12.211615Z
Cauchy-Schwarz Inequality for a Positive Semi-Definite Self-Adjoint Operator
lemmalem:positive-semidefinite-cauchy-schwarz-2026bAnalysis Linear Algebra
Let $V$ together with $\langle\cdot,\cdot\rangle$ be a complex inner product space with zero vector $0_{V}$ , and let $T$ be a linear operator on $V$ that is self-adjoint and positive semi-definite. Let $|z|$ denote the modulus of a complex number $z$ . Then the following hold.…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:34:45.041526Z
A Linear Subspace is a Vector Space and Inherits an Inner Product
lemmalem:subspace-inner-product-space-2026bAnalysis Algebra Linear Algebra
Let $K$ be a field, let $V$ be a vector space over $K$ with zero vector $0_{V}$ , and let $W$ be a linear subspace of $V$ . Then the following hold. 1. (Vector space) The set $W$ , equipped with the restrictions to $W$ of the addition and the scalar multiplication of $V$ , is a vect…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:34:38.892784Z
The Span of a Finite Family is the Smallest Subspace Containing It
lemmalem:span-is-subspace-2026bAlgebra Linear Algebra
Let $K$ be a field, let $V$ be a vector space over $K$ , let $n$ be a natural number, let $[n]$ be the initial segment determined by $n$ , let $v\in V^{n}$ be an $n$ -tuple in $V$ with components $v_{k}$ , and let $\operatorname{span}(v)$ be its span. Then the following hold.…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:34:20.469367Z
Finite-Dimensional Vector Space
definitiondef:finite-dimensional-vector-space-2026bAlgebra Linear Algebra
Let $K$ be a field and let $V$ be a vector space over $K$ with zero vector $0_{V}$ . The space $V$ is finite-dimensional if $V=\{0_{V}\}$ , or if there exist a natural number $n$ and an $n$ -tuple $e\in V^{n}$ that is a basis of $V$ .
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:34:14.833470Z
Span of a Finite Family of Vectors
definitiondef:span-finite-family-2026bAlgebra Linear Algebra
Let $K$ be a field, let $V$ be a vector space over $K$ , let $n$ be a natural number, and let $v\in V^{n}$ be an $n$ -tuple in $V$ , with components $v_{k}$ . The span of $v$ is the set…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:34:11.526107Z
Coordinate Isometry Determined by a Finite Orthonormal Basis
lemmalem:coordinate-isometry-orthonormal-basis-2026cAnalysis Linear Algebra
Let $V$ together with $\langle\cdot,\cdot\rangle$ be a complex inner product space with zero vector $0_{V}$ and induced norm $\lVert\cdot\rVert$ , and let $d$ be the map with $d(u,v)=\lVert u-v\rVert$ , which is a metric on $V$ by claim 3 of…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:14:25.141197Z
Extreme Value Theorem on a Compact Subset of a Metric Space
theoremthm:extreme-value-compact-metric-2026bAnalysis Topology
Let $(X,d)$ be a metric space, equipped with the collection of all subsets that are open in $(X,d)$ , which is a topology by Metric Open Sets Form a Topology. Let $K\subseteq X$ be nonempty and compact in $X$ . Let $\mathbb{R}$ be the set of real numbers with the order $\le$ of its…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:14:13.056205Z
A Distance-Preserving Bijection is a Homeomorphism
lemmalem:distance-preserving-bijection-homeomorphism-2026bAnalysis Topology
Let $(X,d_{X})$ and $(Y,d_{Y})$ be metric spaces. Equip $X$ with the collection $\mathcal{T}_{d_{X}}$ of all subsets that are open in $(X,d_{X})$ , which is a topology by Metric Open Sets Form a Topology, and equip $Y$ with the corresponding collection $\mathcal{T}_{d_{Y}}$ . Write…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:14:04.095251Z
Restriction of a Continuous Map, and Continuous Images of Compact Subsets
lemmalem:continuous-restriction-compact-image-2026bTopology
Let $(X,\mathcal{T}_{X})$ and $(Y,\mathcal{T}_{Y})$ be topological spaces, let $f:X\to Y$ be a continuous map, and let $A\subseteq X$ be equipped with the subspace topology $\mathcal{T}_{A}$ . Let $f|_{A}:A\to Y$ denote the map with $f|_{A}(x)=f(x)$ for every $x\in A$ , and write…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:13:57.186262Z
Concatenation of Finite Sums
lemmalem:finite-sum-concatenation-2026bAnalysis Algebra
Let $K$ be a field. Let $\mathbb{N}$ be the set of natural numbers, with addition $+$ and successor map $S$ as in that definition, and for a natural number $p$ let $[p]$ be the initial segment determined by $p$ , that is, the set of natural numbers $k$ with $1\le k\le p$ . Let…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:13:48.718428Z
Greatest Element of a Finite Family in a Totally Ordered Set
lemmalem:finite-family-greatest-element-2026bSet Theory
Let $A$ be a set equipped with a total order $\le$ , let $n$ be a natural number, let $[n]$ be the initial segment determined by $n$ , and let $c\in A^{n}$ be an $n$ -tuple in $A$ , with components $c_{k}$ . Then there exists $j\in[n]$ such that $c_{k}\le c_{j}$ for every $k\in[n]$ .
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-03T00:13:44.079712Z
Self-Adjointness, Unitarity and Orthogonal Projections Through the Adjoint in Finite Dimensions
lemmalem:operator-classes-via-adjoint-2026dAnalysis Linear Algebra
Let $V$ together with $\langle\cdot,\cdot\rangle$ be a complex inner product space that has an orthonormal basis $e\in V^{n}$ for some natural number $n$ , where $V^{n}$ is the set of $n$ -tuples in $V$ . By Uniqueness of the Adjoint, and Existence in Finite Dimensions every…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-02T20:57:11.365268Z
Every Linear Operator on a Space with a Finite Orthonormal Basis is Bounded
lemmalem:finite-orthonormal-basis-operator-bounded-2026bAnalysis Linear Algebra
Let $V$ together with $\langle\cdot,\cdot\rangle$ be a complex inner product space with induced norm $\lVert\cdot\rVert$ , which is a norm on $V$ by claim 2 of The Induced Norm is a Norm, and Induces a Metric. Let $n$ be a natural number, let $e\in V^{n}$ be an $n$ -tuple in $V$ th…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-02T20:55:50.113931Z

Showing 961-980 of 1428

Back Next

A Finite Sum of Vectors with Vanishing Tail

Any Two Orthonormal Bases of a Complex Inner Product Space Have the Same Size

Interchange of a Finite Double Sum

The Sum of nnn Ones is Strictly Increasing in nnn

Tuples in a Set

Dropping a Redundant Vector from a Spanning Family

Extraction of a Summand from a Finite Sum of Vectors

Cauchy-Schwarz Inequality for a Positive Semi-Definite Self-Adjoint Operator

A Linear Subspace is a Vector Space and Inherits an Inner Product

The Span of a Finite Family is the Smallest Subspace Containing It

Finite-Dimensional Vector Space

Span of a Finite Family of Vectors

Coordinate Isometry Determined by a Finite Orthonormal Basis

Extreme Value Theorem on a Compact Subset of a Metric Space

A Distance-Preserving Bijection is a Homeomorphism

Restriction of a Continuous Map, and Continuous Images of Compact Subsets

Concatenation of Finite Sums

Greatest Element of a Finite Family in a Totally Ordered Set

Self-Adjointness, Unitarity and Orthogonal Projections Through the Adjoint in Finite Dimensions

Every Linear Operator on a Space with a Finite Orthonormal Basis is Bounded

The Sum of $n$ Ones is Strictly Increasing in $n$