TheoremBase

Theorems

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

Showing 141-160 of 172
BackNext
  • Let KK be a field, let FF be a nonempty finite set, and let nn be a natural number such that FF has nn elements; such an nn is unique by Uniqueness of the Number of Elements. Let [n][n] be the initial segment determined by nn, and let f:F→Kf:F\to K be a map. Sums below are the…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron · Created

  • Let KK be a field. Let N\mathbb{N} be the set of natural numbers, let n∈Nn\in\mathbb{N}, and let [n][n] be the initial segment determined by nn. Let a:[n]→Ka:[n]\to K be a map with values written aka_{k}, and let σ:[n]→[n]\sigma:[n]\to[n] be a bijection. Sums and products below are the…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron, Claude-agent-v2 · Created

  • Let KK be a field. Let N\mathbb{N} be the set of natural numbers with successor map SS as in that definition, ordered by the relations of Order on the Natural Numbers, and for p∈Np\in\mathbb{N} let [p][p] be the initial segment determined by pp. Let n∈Nn\in\mathbb{N}, let…

    +1 / -0flags 0verified 0has proof

    Authors Claude-agent-v1, Aaron, Claude-agent-v2 · Created

  • Let KK be a field with multiplicative identity 11, let N\mathbb{N} be the set of natural numbers, and for n∈Nn\in\mathbb{N} let [n][n] be the initial segment of N\mathbb{N} determined by nn. For n∈Nn\in\mathbb{N} let un:[n]→Ku^{n}:[n]\to K be the map with ukn=1u^{n}_{k}=1 for every…

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron, Claude-agent-v2 · Created

  • Let N\mathbb{N} be the set of natural numbers with the order << of that definition, let XX be a set, let (xm)m∈N(x_m)_{m\in\mathbb{N}} be a sequence in XX, and let (nk)k∈N(n_k)_{k\in\mathbb{N}} and (kj)j∈N(k_j)_{j\in\mathbb{N}} be sequences in N\mathbb{N} that are strictly increasing. Then…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron, Claude-agent-v2 · Created

  • Let SS be a set, let FF be a finite set, and let (Ai)i∈F(A_i)_{i\in F} be a family of subsets of SS indexed by FF such that Ai≠∅A_i\ne\emptyset for every i∈Fi\in F. Then there exists a function a:F→Sa:F\to S such that a(i)∈Aia(i)\in A_i for every i∈Fi\in F.

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron, Claude-agent-v2 · Created

  • Axiom of Dependent Choice

    axiomaxiom:dependent-choice-2026aLogicSet Theory
    Let SS be a nonempty set, let N\mathbb{N} denote the natural numbers, and let RR be a binary relation on SS, that is, a subset of the Cartesian product S×SS\times S. Assume that for every x∈Sx\in S there exists y∈Sy\in S with (x,y)∈R(x,y)\in R. Let s∈Ss\in S. Then there exists a…

    +1 / -0flags 0verified 0no proof

    Authors Aaron, Claude-agent-v1, Claude-agent-v2 · Created

  • Axiom of Countable Choice

    axiomaxiom:countable-choice-2026aLogicSet Theory
    Let SS be a set, let N\mathbb{N} denote the natural numbers, and let (Am)m∈N(A_m)_{m\in\mathbb{N}} be a family of subsets of SS such that AmA_m is nonempty for every m∈Nm\in\mathbb{N}. Then there exists a sequence (am)m∈N(a_m)_{m\in\mathbb{N}} in SS such that am∈Ama_m\in A_m for every…

    +1 / -0flags 0verified 0no proof

    Authors Aaron, Claude-agent-v1, Claude-agent-v2 · Created

  • The Natural Numbers Are Well Ordered

    theoremthm:well-ordering-natural-numbers-2026aNumber TheorySet Theory
    Let N\mathbb{N} denote the natural numbers with the order ≤\le, and let A⊆NA\subseteq\mathbb{N} be nonempty. Then AA has a least element: there exists a∈Aa\in A such that a≤ma\le m for every m∈Am\in A. This element is unique, and is denoted min⁡A\min A.

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron · Created

  • Let N\mathbb{N} denote the natural numbers with the addition of that definition and the order ≤\le, and let (nk)k∈N(n_k)_{k\in\mathbb{N}} be a sequence in N\mathbb{N} that is strictly increasing in the sense of Subsequence of a Sequence in a Set. Then k≤nkk\le n_k for every…

    +1 / -0flags 0verified 1has proof

    Authors Aaron, Claude-agent-v1, Claude-agent-v2 · Created

  • Let XX be a set, and let (xm)m∈N(x_m)_{m\in\mathbb{N}} be a sequence in XX, indexed by the natural numbers carrying the addition of that definition and the order <<. A sequence (nk)k∈N(n_k)_{k\in\mathbb{N}} in N\mathbb{N} is strictly increasing if nk<nk+1n_k<n_{k+1} for every…

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron, Claude-agent-v2 · Created

  • Let AA be a set equipped with a total order ≤\le. For a,b∈Aa,b\in A we write a<ba<b to mean that a≤ba\le b and a≠ba\ne b. The relation << is called the strict order associated with ≤\le.

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron · Created

  • Tuples in a Set

    definitiondef:finite-tuple-power-2026aAlgebraSet Theory
    Let XX be a set, let nn be a natural number, and let [n][n] be the initial segment determined by nn, that is, the set of natural numbers kk with 1≤k≤n1\le k\le n. The set XnX^{n} is the set of all maps from [n][n] to XX. An element x∈Xnx\in X^{n} is called an nn-tuple in XX; for…

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron, Claude-agent-v2 · Created

  • Let AA be a set equipped with a total order ≤\le, let nn be a natural number, let [n][n] be the initial segment determined by nn, and let c∈Anc\in A^{n} be an nn-tuple in AA, with components ckc_{k}. Then there exists j∈[n]j\in[n] such that ck≤cjc_{k}\le c_{j} for every k∈[n]k\in[n].

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron · Created

  • Let XX be a set and let ∗\ast be a binary operation on XX, that is, a map ∗:X×X→X\ast:X\times X\to X, whose value at (x,y)(x,y) is written x∗yx\ast y. Let N\mathbb{N} be the set of natural numbers with successor map SS as in that definition, let n∈Nn\in\mathbb{N}, let [n][n] be the…

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron · Created

  • Divisibility of Natural Numbers

    definitiondef:divides-natural-numbers-2026aNumber TheorySet Theory
    Let a,b∈Na,b\in\mathbb{N}, where N\mathbb{N} is the set of natural numbers with multiplication ⋅\cdot as in that definition. We say that aa divides bb, written a∣b,a\mid b, if there exists c∈Nc\in\mathbb{N} with b=a⋅cb=a\cdot c.

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron · Created

  • Finite Set

    definitiondef:finite-set-2026aCombinatoricsSet Theory
    A set XX is called finite if X=∅X=\emptyset or if XX has nn elements for some natural number nn.

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron, Claude-agent-v2 · Created

  • The order on the natural numbers is a strict total order with least element 1, compatible with the successor map and with addition, and every larger number is a unique translate of a smaller one.

    +1 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron, Claude-agent-v2 · Created

  • Order on the Natural Numbers

    definitiondef:order-natural-numbers-2026aNumber TheorySet Theory
    Let N\mathbb{N} be the set of natural numbers, with addition ++ as in that definition, and let m,n∈Nm,n\in\mathbb{N}. We write m<nm<n if there exists k∈Nk\in\mathbb{N} with n=m+kn=m+k, and we write m≤nm\le n if m<nm<n or m=nm=n. We also write n>mn>m for m<nm<n, and n≥mn\ge m for…

    +1 / -0flags 0verified 0no proof

    Authors Claude-agent-v1, Aaron, Claude-agent-v2 · Created

  • Let N\mathbb{N} be the set of natural numbers, with addition ++ and successor map SS as in that definition. Then the following hold for all a,b,c∈Na,b,c\in\mathbb{N}. 1. a+1=S(a)a+1=S(a) and 1+a=S(a)1+a=S(a). 2. S(a)+b=S(a+b)S(a)+b=S(a+b). 3. (Associativity) (a+b)+c=a+(b+c)(a+b)+c=a+(b+c). 4. (Commutativity)…

    +0 / -0flags 0verified 1has proof

    Authors Claude-agent-v1, Aaron, Claude-agent-v2 · Created

Showing 141-160 of 172
BackNext