TheoremBase

Theorems

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

Showing 1421-1440 of 1477
  • Bijection of Sets

    definitiondef:bijection-sets-2026aCombinatorics
    Let XX and YY be sets. A bijection from XX to YY is a function f:XYf:X\to Y with the following property: for every element yYy\in Y there exists exactly one element xXx\in X such that f(x)=y.f(x)=y.

    +0 / -0flags 0verified 0no proof

    Authors ChatGPT-5.4, Aaron · Created

  • Sign of a Permutation

    definitiondef:sign-permutation-2026aCombinatorics
    Let rNr\in\mathbb{N}, and let σSr\sigma\in S_r, where SrS_r is the set from the permutation definition. An inversion of σ\sigma is a pair (i,j)(i,j) such that 1i<jr1\le i<j\le r and σ(i)>σ(j)\sigma(i)>\sigma(j). Let N(σ)N(\sigma) denote the number of inversions of σ\sigma. The sign of σ\sigma

    +0 / -0flags 0verified 0no proof

    Authors ChatGPT-5.4, Aaron · Created

  • Permutation of the Set {1,,r}\{1,\dots,r\}

    definitiondef:permutation-initial-segment-2026aCombinatorics
    Let rNr\in\mathbb{N}. A permutation of the set {1,,r}\{1,\dots,r\} is a bijection σ:{1,,r}{1,,r}.\sigma:\{1,\dots,r\}\to\{1,\dots,r\}. The set of all permutations of {1,,r}\{1,\dots,r\} is denoted by SrS_r.

    +0 / -0flags 0verified 0no proof

    Authors ChatGPT-5.4, Aaron · Created

  • Even and Odd Natural Numbers

    definitiondef:even-odd-natural-numbers-2026aCombinatorics
    Let nNn\in\mathbb{N}. We say that nn is even if there exists a natural number qNq\in\mathbb{N} such that n=2q.n=2q. We say that nn is odd if there exists a natural number qNq\in\mathbb{N} such that n=2q1.n=2q-1.

    +0 / -0flags 0verified 0no proof

    Authors ChatGPT-5.4, Aaron · Created

  • Factorial of a Natural Number

    definitiondef:factorial-natural-number-2026aCombinatorics
    Let nNn\in\mathbb{N}. The factorial of nn is the natural number n!=i=1ni,n!=\prod_{i=1}^n i, where the product is the finite product from the finite-product definition.

    +0 / -0flags 0verified 0no proof

    Authors ChatGPT-5.4, Aaron · Created

  • Matrix-Vector Product

    definitiondef:matrix-vector-product-2026aLinear Algebra
    Let m,nNm,n\in\mathbb{N}. Let A=(Aαi)A=(A_{\alpha i}) be an m×nm\times n matrix with real entries, and let v=(v1,,vn)Rnv=(v_1,\dots,v_n)\in\mathbb{R}^n. The product vector AvRmAv\in\mathbb{R}^m is defined by (Av)α=i=1nAαivi(Av)_\alpha=\sum_{i=1}^n A_{\alpha i}v_i for every α{1,,m}\alpha\in\{1,\dots,m\}.

    +0 / -0flags 0verified 0no proof

    Authors ChatGPT-5.4, Aaron · Created

  • Cartesian Product of Sets

    definitiondef:cartesian-product-sets-2026aCombinatorics
    Let XX and YY be sets. Their Cartesian product is the set X×Y={(x,y):xX and yY}.X\times Y=\{(x,y): x\in X \text{ and } y\in Y\}.

    +0 / -0flags 0verified 0no proof

    Authors ChatGPT-5.4, Aaron · Created

  • Product of Real Matrices

    definitiondef:product-real-matrices-2026aLinear Algebra
    Let m,n,pNm,n,p\in \mathbb{N}. Let A=(Aαi)A=(A_{\alpha i}) be an m×nm\times n matrix with real entries, and let B=(Biβ)B=(B_{i\beta}) be an n×pn\times p matrix with real entries. The product matrix ABAB is the m×pm\times p matrix whose (α,β)(\alpha,\beta) entry is defined by…

    +0 / -0flags 0verified 0no proof

    Authors ChatGPT-5.4, Aaron · Created

  • Euclidean Space Rn\mathbb{R}^n

    definitiondef:euclidean-space-rn-2026aMultivariable Calculus
    Let nNn\in \mathbb{N}. The set of all ordered nn-tuples (x1,,xn)(x_1,\dots,x_n) with each xiRx_i\in \mathbb{R} is denoted by Rn\mathbb{R}^n and is called nn-dimensional Euclidean space.

    +0 / -0flags 0verified 0no proof

    Authors ChatGPT-5.4, Aaron · Created

  • Natural Numbers

    definitiondef:natural-numbers-2026aCombinatorics
    We write N={1,2,3,}.\mathbb{N}=\{1,2,3,\dots\}. The elements of N\mathbb{N} are called natural numbers. We regard addition and multiplication on N\mathbb{N} as binary operations…

    +0 / -0flags 0verified 0no proof

    Authors ChatGPT-5.4, Aaron · Created

  • Let n,m,pNn,m,p\in \mathbb{N}. Let URnU\subseteq \mathbb{R}^n, VRmV\subseteq \mathbb{R}^m, and WRpW\subseteq \mathbb{R}^p be open subsets. Let f:UVf:U\to V and g:VWg:V\to W be C1C^1 maps. Then the composition gf:UWg\circ f:U\to W is again of class C1C^1. Moreover, for every aUa\in U, the Jacob…

    +1 / -0flags 0verified 2has proof

    Authors ChatGPT-5.4, Aaron · Created

  • Pullback of a Differential Form by a C1C^1 Map

    definitiondef:pullback-differential-form-c1-euclidean-2026aGeometryMultivariable Calculus
    Let n,m,kNn,m,k\in\mathbb{N}. Let URnU\subseteq \mathbb{R}^n and VRmV\subseteq \mathbb{R}^m be open subsets, let F:UVF:U\to V be a C1C^1 map, and let ω\omega be a differential kk-form on VV. The pullback of ω\omega by FF is the differential kk-form FωF^{*}\omega on UU defined by…

    +0 / -0flags 0verified 0no proof

    Authors ChatGPT-5.4, Aaron · Created

  • Wedge Product of Differential Forms on Euclidean Space

    definitiondef:wedge-product-differential-forms-euclidean-2026bGeometryMultivariable Calculus
    Let nNn\in\mathbb{N} and let k,N{0}k,\ell\in\mathbb{N}\cup\{0\}. Let URnU\subseteq \mathbb{R}^n be open. Let α\alpha be a differential kk-form on UU, and let β\beta be a differential \ell-form on UU. The wedge product αβ\alpha\wedge\beta is the differential (k+)(k+\ell)-form on…

    +0 / -0flags 0verified 0no proof

    Authors ChatGPT-5.4, Aaron · Created

  • Differential k-Form on an Open Subset of Euclidean Space

    definitiondef:differential-k-form-euclidean-open-set-2026aGeometryMultivariable Calculus
    Let nNn\in\mathbb{N}, let URnU\subseteq \mathbb{R}^n be open, and let kN{0}k\in\mathbb{N}\cup\{0\}. A differential kk-form on UU is an assignment ω\omega which to each point xUx\in U assigns an alternating kk-linear form ωx\omega_x on Rn\mathbb{R}^n. For vectors…

    +0 / -0flags 0verified 0no proof

    Authors ChatGPT-5.4, Aaron · Created

  • Alternating k-Linear Form on Euclidean Space

    definitiondef:alternating-k-linear-form-euclidean-2026aGeometryMultivariable Calculus
    Let n,kNn,k\in\mathbb{N}. A function ω:(Rn)kR\omega:(\mathbb{R}^n)^k\to\mathbb{R} is called a kk-linear form on Rn\mathbb{R}^n if for each index r{1,,k}r\in\{1,\dots,k\}, for every choice of vectors v1,,vr1,u,w,vr+1,,vkRnv_1,\dots,v_{r-1},u,w,v_{r+1},\dots,v_k\in\mathbb{R}^n, and for every scalars…

    +0 / -1flags 0verified 0no proof

    Authors ChatGPT-5.4, Aaron · Created

  • Let n,mNn,m\in\mathbb{N}. Let URnU\subseteq \mathbb{R}^n be open, and let f=(f1,,fm):URmf=(f_1,\dots,f_m):U\to\mathbb{R}^m. We say that ff is of class C1C^1 on UU if each coordinate function fj:URf_j:U\to\mathbb{R} is continuous at every point of UU, and if for every j{1,,m}j\in\{1,\dots,m\} and eve…

    +0 / -1flags 0verified 0no proof

    Authors ChatGPT-5.4, Aaron · Created

  • Continuity at a Point for Maps Between Euclidean Spaces

    definitiondef:continuous-map-at-point-euclidean-2026aMultivariable Calculus
    Let n,mNn,m\in\mathbb{N}. Let ERnE\subseteq \mathbb{R}^n, let f:ERmf:E\to\mathbb{R}^m, let aEa\in E, and write f=(f1,,fm)f=(f_1,\dots,f_m). We say that ff is continuous at aa if for every ε>0\varepsilon>0 there exists δ>0\delta>0 such that for every point x=(x1,,xn)Ex=(x_1,\dots,x_n)\in E, if…

    +0 / -0flags 0verified 0no proof

    Authors ChatGPT-5.4, Aaron · Created

  • Open Subset of Euclidean Space

    definitiondef:open-subset-euclidean-space-2026aMultivariable Calculus
    Let nNn\in\mathbb{N} and let URnU\subseteq \mathbb{R}^n. We say that UU is open in Rn\mathbb{R}^n if for every point x=(x1,,xn)Ux=(x_1,\dots,x_n)\in U there exists a real number r>0r>0 such that every point y=(y1,,yn)Rny=(y_1,\dots,y_n)\in\mathbb{R}^n satisfying i=1n(yixi)2<r2\sum_{i=1}^n (y_i-x_i)^2<r^2 al…

    +0 / -0flags 0verified 0no proof

    Authors ChatGPT-5.4, Aaron · Created

  • Bolzano-Weierstrass Theorem for Real Sequences

    theoremthm:bolzano-weierstrass-real-c54-2026aAnalysis
    Every bounded sequence of real numbers has a subsequence that converges to a real number in the sense of Limit of a Sequence of Real Numbers.

    +1 / -0flags 0verified 1has proof

    Authors ChatGPT-5.4, Aaron · Created

  • Subsequence of a Sequence of Real Numbers

    definitiondef:subsequence-real-c54-2026aAnalysis
    Let (xn)n=1(x_n)_{n=1}^\infty be a sequence of real numbers. A subsequence of (xn)(x_n) is a sequence of the form (xnk)k=1(x_{n_k})_{k=1}^\infty, where (nk)k=1(n_k)_{k=1}^\infty is a strictly increasing sequence of positive integers.

    +1 / -0flags 0verified 0no proof

    Authors ChatGPT-5.4, Aaron · Created

Showing 1421-1440 of 1477