Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Cauchy-Schwarz Inequality for a Positive Semi-Definite Self-Adjoint Operator
lemmalem:positive-semidefinite-cauchy-schwarz-2026bAnalysisLinear AlgebraLet together with be a complex inner product space with zero vector , and let be a linear operator on that is self-adjoint and positive semi-definite. Let denote the modulus of a complex number . Then the following hold.…A Linear Subspace is a Vector Space and Inherits an Inner Product
lemmalem:subspace-inner-product-space-2026bAnalysisAlgebraLinear AlgebraLet be a field, let be a vector space over with zero vector , and let be a linear subspace of . Then the following hold. 1. (Vector space) The set , equipped with the restrictions to of the addition and the scalar multiplication of , is a vect…The Span of a Finite Family is the Smallest Subspace Containing It
lemmalem:span-is-subspace-2026cLinear AlgebraThe span of a finite family is a linear subspace containing each vector of the family, and it is contained in every subspace that contains them.Finite-Dimensional Vector Spaces and Their Dimension
definitiondef:finite-dimensional-vector-space-2026cLinear AlgebraA vector space is finite-dimensional when some finite family spans it, and its dimension is then the common length of its bases.- The span of a finite family of vectors is the set of its linear combinations, and the family spans the space when its span is the whole space.
Coordinate Isometry Determined by a Finite Orthonormal Basis
lemmalem:coordinate-isometry-orthonormal-basis-2026cAnalysisLinear AlgebraLet together with be a complex inner product space with zero vector and induced norm , and let be the map with , which is a metric on by claim 3 of…Extreme Value Theorem on a Compact Subset of a Metric Space
theoremthm:extreme-value-compact-metric-2026cAnalysisTopologyA real-valued function that is continuous on a nonempty compact subset of a metric space attains a minimum and a maximum on it.A Distance-Preserving Bijection is a Homeomorphism
lemmalem:distance-preserving-bijection-homeomorphism-2026bAnalysisTopologyLet and be metric spaces. Equip with the collection of all subsets that are open in , which is a topology by The Open Subsets of a Metric Space Form a Topology, and equip with the corresponding collection…Restriction of a Continuous Map, and Continuous Images of Compact Subsets
lemmalem:continuous-restriction-compact-image-2026bTopologyLet and be topological spaces, let be a continuous map, and let be equipped with the subspace topology . Let denote the map with for every , and write…- Let be a field. Let be the set of natural numbers, with addition and successor map as in that definition, and for a natural number let be the initial segment determined by , that is, the set of natural numbers with . Let…
Greatest Element of a Finite Family in a Totally Ordered Set
lemmalem:finite-family-greatest-element-2026bSet TheoryLet be a set equipped with a total order , let be a natural number, let be the initial segment determined by , and let be an -tuple in , with components . Then there exists such that for every .Self-Adjointness, Unitarity and Orthogonal Projections Through the Adjoint in Finite Dimensions
lemmalem:operator-classes-via-adjoint-2026dAnalysisLinear AlgebraLet together with be a complex inner product space that has an orthonormal basis for some natural number , where is the set of -tuples in . By Uniqueness of the Adjoint, and Existence in Finite Dimensions every…Every Linear Operator on a Space with a Finite Orthonormal Basis is Bounded
lemmalem:finite-orthonormal-basis-operator-bounded-2026bAnalysisLinear AlgebraLet together with be a complex inner product space with induced norm , which is a norm on by claim 2 of The Induced Norm is a Norm, and Induces a Metric. Let be a natural number, let be an -tuple in th…- Let be a complex vector space equipped with a norm , let and be bounded linear operators on , and let be a complex number with modulus . Write and for their…
- Let be a complex vector space equipped with a norm , let be a bounded linear operator on , and let be a real number. The number is an operator norm of if is a bound for and …
Existence and Uniqueness of the Operator Norm
lemmalem:operator-norm-existence-uniqueness-2026aAnalysisLinear AlgebraLet be a complex vector space equipped with a norm , and let be a bounded linear operator on . Let denote the set of those real numbers that are of the form for some with , the order being that…Bound for a Linear Operator and Bounded Linear Operator
definitiondef:bounded-linear-operator-2026aAnalysisLinear AlgebraLet be a complex vector space equipped with a norm , let be a linear operator on , and let be a real number with , the order being that of the ordered field of real numbers. The number is a bound for if…Triangle Inequality for Finite Sums of Vectors
lemmalem:finite-sum-norm-triangle-2026aAnalysisLinear AlgebraLet be a complex vector space equipped with a norm , let be a natural number, let be the initial segment determined by , and let be a map with values . Then…- Let together with be a complex inner product space with zero vector , and let be a linear operator on . The operator is positive definite if for every the complex number is a real number satisfyin…
- Let together with be a complex inner product space, with induced norm , which is a norm on by claim 2 of The Induced Norm is a Norm, and Induces a Metric. Let be a unitary operator on . Throughout, …