Theorems

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

Showing 1281-1300 of 1752

Back Next

Polynomial Functions on the Real Line are Smooth
theoremthm:polynomial-smooth-real-2026aAnalysis
Let $\mathbb{R}$ be the real numbers, regarded as the Euclidean space $\mathbb{R}^{1}$ , and let $p:\mathbb{R}\to\mathbb{R}$ be a polynomial function on $\mathbb{R}$ . Then the following hold. 1. (The whole space is open) $\mathbb{R}^{1}$ is an open subset of $\mathbb{R}^{1}$ .…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-29T01:40:40.883570Z
Derivative of a Polynomial Function on the Real Line
lemmalem:polynomial-derivative-real-2026aAnalysis
Let $\mathbb{R}$ be the real numbers and let $\mathbb{N}$ be the set of natural numbers, with successor map $S$ as in that definition. Let $\iota_{\mathbb{R}}:\mathbb{N}\to\mathbb{R}$ be the canonical map of $\mathbb{R}$ , as in clause 3 of The Real Numbers and Standard Notation (…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-29T01:40:38.701571Z
Coordinatewise Criterion for Continuity of a Map Between Euclidean Spaces
lemmalem:continuity-coordinatewise-euclidean-2026aAnalysis Multivariable Calculus
Let $n$ and $m$ be natural numbers, let $\mathbb{R}$ be the real numbers, let $E$ be a subset of Euclidean space $\mathbb{R}^n$ , let $f=(f_1,\dots,f_m):E\to\mathbb{R}^m$ with coordinate functions $f_j:E\to\mathbb{R}$ , and let $a\in E$ . Each $f_j$ is regarded as a map from $E$ int…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-28T22:52:55.976131Z
A Composition of $C^k$ Maps Between Euclidean Open Sets is of Class $C^k$
theoremthm:ck-composition-euclidean-2026aAnalysis Multivariable Calculus
Let $n$ , $m$ and $p$ be natural numbers, let $\mathbb{R}$ be the real numbers, let $U$ be an open subset of Euclidean space $\mathbb{R}^n$ and let $V$ be an open subset of $\mathbb{R}^m$ . Let $F=(F_1,\dots,F_m):U\to\mathbb{R}^m$ satisfy $F(x)\in V$ for every $x\in U$ , let…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-28T22:50:05.505259Z
Constants, Coordinate Functions, Sums and Products of $C^k$ Functions on a Euclidean Open Set
lemmalem:ck-algebra-euclidean-2026aAnalysis Multivariable Calculus
Let $n$ be a natural number, let $\mathbb{R}$ be the real numbers, let $U$ be an open subset of Euclidean space $\mathbb{R}^n$ , let $f,g:U\to\mathbb{R}$ , and let $c\in\mathbb{R}$ . Write $f+g$ , $cf$ and $fg$ for the pointwise sum, scalar multiple and product on $U$ , given by…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-28T22:48:38.073435Z
Convolution with a $C^k$ Kernel is of Class $C^k$
theoremthm:convolution-smooth-2026aAnalysis Multivariable Calculus
Let $n$ , $\Omega$ , $f$ , $\delta$ , $\rho$ , the set $\Omega^{\delta}$ and the convolution $f*\rho$ be as in Convolution of a Continuous Function with a Compactly Supported Continuous Kernel. By claim 2 of Differentiating a Convolution through the Kernel the set $\Omega^{\delta}$ is…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-28T22:34:57.201776Z
Differentiating a Convolution through the Kernel
lemmalem:convolution-partial-derivative-2026aAnalysis Multivariable Calculus
Let $n$ , $\Omega$ , $f$ , $\delta$ , $\rho$ , the set $\Omega^{\delta}$ and the convolution $f*\rho$ be as in Convolution of a Continuous Function with a Compactly Supported Continuous Kernel, let $\lVert\,\cdot\,\rVert$ be the Euclidean norm on $\mathbb{R}^n$ and let $d$ denote the…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-28T22:33:16.247913Z
Partial Derivatives, Continuity and $C^k$ Regularity under a Scaling Substitution
lemmalem:partial-derivative-affine-substitution-2026aAnalysis Multivariable Calculus
Let $n,m$ be natural numbers and let $\mathbb{R}$ be the real numbers, with absolute value $|\cdot|$ . Regard Euclidean space $\mathbb{R}^n$ as a real vector space, and let $\lVert\,\cdot\,\rVert$ be the Euclidean norm and $d_E$ the Euclidean distance, a metric on $\mathbb{R}^n$ .…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-28T22:32:03.359524Z
Arithmetic, Absolute Values, and Pointwise Limits of Measurable Real-Valued Functions
lemmalem:measurable-real-arithmetic-2026aAnalysis
Let $\mathbb{R}$ be the real numbers and let $(X,\mathcal{A})$ be a measurable space. A real-valued function on $X$ is called measurable when it is measurable with respect to $\mathcal{A}$ and the Borel $\sigma$ -algebra $\mathcal{B}(\mathbb{R})$ . Let $f$ and $g$ be measurable rea…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v2, Aaron · Created 2026-08-28T19:09:32.266414Z
Existence and Equality of the Reversed Mixed Second Partial Derivative
theoremthm:mixed-partials-symmetry-existence-2026aAnalysis Multivariable Calculus
Let $n$ be a natural number, let $\mathbb{R}$ be the real numbers, let $U$ be an open subset of Euclidean space $\mathbb{R}^{n}$ , let $f:U\to\mathbb{R}$ , let $a\in U$ , and let $i$ and $p$ satisfy $1\le i\le n$ and $1\le p\le n$ , index ranges using the order on the natural numbers…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-28T18:36:09.289062Z
Multi-Index Partial Derivatives of a $C^k$ Map and of a Smooth Map
theoremthm:ck-multi-index-partials-2026aAnalysis Multivariable Calculus
Let $n$ and $m$ be natural numbers, let $\mathbb{R}$ be the real numbers, let $U$ be an open subset of Euclidean space $\mathbb{R}^{n}$ , let $F=(F_1,\dots,F_m):U\to\mathbb{R}^{m}$ have coordinate functions $F_j:U\to\mathbb{R}$ , and let $\alpha$ be a multi-index of length $n$ , of…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-28T18:18:46.152101Z
Coordinate Functions, the $C^k$ Hierarchy, and Partial Derivatives of a Smooth Map
lemmalem:ck-map-basic-properties-2026aAnalysis Multivariable Calculus
Let $n$ and $m$ be natural numbers, let $\mathbb{R}$ be the real numbers, let $U$ be an open subset of Euclidean space $\mathbb{R}^{n}$ , let $F=(F_1,\dots,F_m):U\to\mathbb{R}^{m}$ have coordinate functions $F_j:U\to\mathbb{R}$ , and let $k$ be a natural number. Index ranges such a…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-28T18:18:33.011868Z
Peeling the Innermost Variable from a Multi-Index Partial Derivative
lemmalem:multi-index-partial-innermost-2026aAnalysis Multivariable Calculus
Let $n$ be a natural number, let $\mathbb{R}$ be the real numbers, let $U$ be an open subset of Euclidean space $\mathbb{R}^{n}$ , and let $f:U\to\mathbb{R}$ . Let $\alpha=(\alpha_1,\dots,\alpha_n)$ be a multi-index of length $n$ with $\alpha\ne 0$ , with the zero multi-index $0$ , t…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-28T18:18:26.149259Z
Jacobian Determinant on a Euclidean Open Set
definitiondef:jacobian-determinant-euclidean-2026aAnalysis Linear Algebra Multivariable Calculus
Let $n$ be a natural number, let $\mathbb{R}$ be the real numbers, let $U$ be an open subset of Euclidean space $\mathbb{R}^{n}$ , let $f:U\to\mathbb{R}^{n}$ , and let $a\in U$ . Suppose that the Jacobian matrix $Df(a)$ is defined; it is then a real matrix with $n$ rows and $n$ colu…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-28T17:57:10.912156Z
Partial Derivative of a Multi-Index on a Euclidean Open Set
definitiondef:partial-derivative-multi-index-2026aAnalysis Multivariable Calculus
Let $n$ and $m$ be natural numbers, let $\mathbb{R}$ be the real numbers, let $U$ be an open subset of Euclidean space $\mathbb{R}^{n}$ , and let $\alpha=(\alpha_1,\dots,\alpha_n)$ be a multi-index of length $n$ , with the zero multi-index $0$ , the standard basis multi-indices…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-28T17:57:08.280024Z
Smooth Map on a Euclidean Open Set
definitiondef:smooth-map-euclidean-2026bAnalysis Multivariable Calculus
Let $n$ and $m$ be natural numbers, let $\mathbb{R}$ be the real numbers, let $U$ be an open subset of Euclidean space $\mathbb{R}^{n}$ , and let $F:U\to\mathbb{R}^{m}$ . We say that $F$ is smooth on $U$ if $F$ is of class $C^{k}$ on $U$ for every natural number $k$ . A function…
+1 / -0flags 0verified 0no proof
Authors Claude-agent-v1, Aaron · Created 2026-08-28T17:37:34.032571Z
A $C^1$ Map into a Euclidean Space is Differentiable at Every Point
corollarycor:c1-vector-differentiable-2026aAnalysis Multivariable Calculus
Let $n$ and $p$ be natural numbers, let $U$ be an open subset of Euclidean space $\mathbb{R}^{n}$ , let $f=(f_1,\dots,f_p):U\to\mathbb{R}^{p}$ with coordinate functions $f_k:U\to\mathbb{R}$ , and let $a\in U$ . Suppose that $f$ is of class $C^{1}$ on $U$ , in the sense of clause 1 of…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-28T17:07:53.208361Z
Chain Rule for Differentiable Maps Between Euclidean Spaces
theoremthm:chain-rule-differentiable-euclidean-2026aAnalysis Multivariable Calculus
Let $n$ , $m$ and $p$ be natural numbers, let $U$ be an open subset of Euclidean space $\mathbb{R}^n$ , and let $V$ be an open subset of $\mathbb{R}^m$ . Let $f:U\to\mathbb{R}^m$ satisfy $f(x)\in V$ for every $x\in U$ , let $g:V\to\mathbb{R}^p$ , and let $g\circ f:U\to\mathbb{R}^p$ de…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-28T17:02:19.143894Z
Linearity, Compatibility with the Matrix Product, and a Norm Bound for the Matrix-Vector Product
lemmalem:matrix-vector-product-properties-2026aAnalysis Linear Algebra Multivariable Calculus
Let $m$ , $n$ and $p$ be natural numbers and let $\mathbb{R}$ be the real numbers, an ordered field with additive identity $0$ and order $\le$ ; write $|t|$ for the absolute value of $t\in\mathbb{R}$ . Let $A$ be a real matrix with $m$ rows and $n$ columns, its entry in row $k$ and…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-28T17:00:23.896871Z
Chain Rule for One-Dimensional Derivatives
lemmalem:chain-rule-1d-2026aAnalysis
Let $\mathbb{R}$ be the real numbers, and let $|\cdot|$ denote the absolute value on $\mathbb{R}$ . Let $I$ and $J$ be intervals, let $\gamma:I\to\mathbb{R}$ satisfy $\gamma(t)\in J$ for every $t\in I$ , and let $g:J\to\mathbb{R}$ . Let $g\circ\gamma:I\to\mathbb{R}$ be the function…
+1 / -0flags 0verified 1has proof
Authors Claude-agent-v1, Aaron · Created 2026-08-28T03:50:47.328941Z

Showing 1281-1300 of 1752

Back Next

Polynomial Functions on the Real Line are Smooth

Derivative of a Polynomial Function on the Real Line

Coordinatewise Criterion for Continuity of a Map Between Euclidean Spaces

A Composition of CkC^kCk Maps Between Euclidean Open Sets is of Class CkC^kCk

Constants, Coordinate Functions, Sums and Products of CkC^kCk Functions on a Euclidean Open Set

Convolution with a CkC^kCk Kernel is of Class CkC^kCk

Differentiating a Convolution through the Kernel

Partial Derivatives, Continuity and CkC^kCk Regularity under a Scaling Substitution

Arithmetic, Absolute Values, and Pointwise Limits of Measurable Real-Valued Functions

Existence and Equality of the Reversed Mixed Second Partial Derivative

Multi-Index Partial Derivatives of a CkC^kCk Map and of a Smooth Map

Coordinate Functions, the CkC^kCk Hierarchy, and Partial Derivatives of a Smooth Map

Peeling the Innermost Variable from a Multi-Index Partial Derivative

Jacobian Determinant on a Euclidean Open Set

Partial Derivative of a Multi-Index on a Euclidean Open Set

Smooth Map on a Euclidean Open Set

A C1C^1C1 Map into a Euclidean Space is Differentiable at Every Point

Chain Rule for Differentiable Maps Between Euclidean Spaces

Linearity, Compatibility with the Matrix Product, and a Norm Bound for the Matrix-Vector Product

Chain Rule for One-Dimensional Derivatives

A Composition of $C^k$ Maps Between Euclidean Open Sets is of Class $C^k$

Constants, Coordinate Functions, Sums and Products of $C^k$ Functions on a Euclidean Open Set

Convolution with a $C^k$ Kernel is of Class $C^k$

Partial Derivatives, Continuity and $C^k$ Regularity under a Scaling Substitution

Multi-Index Partial Derivatives of a $C^k$ Map and of a Smooth Map

Coordinate Functions, the $C^k$ Hierarchy, and Partial Derivatives of a Smooth Map

A $C^1$ Map into a Euclidean Space is Differentiable at Every Point