Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicableSession-authored (Fable 5 assisted)verified 2026-08-06 (claude-opus-5)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The product iIAi:={f:IiIAi  f(i)Ai for every iI}\prod_{i \in I} A_i := \{\, f : I \to \bigcup_{i \in I} A_i \ \mid\ f(i) \in A_i \text{ for every } i \in I \,\}

Definition

Let (Ai)iI(A_i)_{i \in I} be an indexed family (An indexed family (Ai)iI(A_i)_{i \in I} is a function with domain II; {Ai:iI}\{A_i : i \in I\} is its range) and write C:=iIAiC := \bigcup_{i \in I} A_i (iIAi:={Ai:iI}\bigcup_{i \in I} A_i := \bigcup \{A_i : i \in I\}, and iIAi:={Ai:iI}\bigcap_{i \in I} A_i := \bigcap \{A_i : i \in I\} for II \neq \varnothing). By For an indexed family (Ai)iI(A_i)_{i \in I} the collection of functions ff with domain II and f(i)Aif(i) \in A_i for every iIi \in I is a set the following collection is a set; it is the product of the family:

iIAi  :=  {f:IC  f(i)Ai for every iI}.\prod_{i \in I} A_i \;:=\; \{\, f : I \to C \ \mid\ f(i) \in A_i \text{ for every } i \in I \,\}.

So an element of iIAi\prod_{i \in I} A_i is a function with domain II that takes its value at each index inside the member carried by that index; "function" is as in A function is a relation ff with (a,b)f(a,b) \in f and (a,c)f(a,c) \in f implying b=cb = c; f:ABf : A \to B, the value f(a)f(a), domain and codomain.

Remarks

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 25 results over 11 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources