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 set of all functions
Definition
Let and be sets. By For sets and the collection of all functions is a set, being a subset of the functions (A function is a relation with and implying ; , the value , domain and codomain) form a set; it is written
Thus holds if and only if .
Remarks
-
The notation collides with exponentiation, and the collision is deliberate. is the same symbol the library already uses for a space of functions in The vector space of all functions with pointwise operations, and as the case ↗, where is the set of functions carrying a vector-space structure; the underlying set there is the one defined here. Some set-theory texts write instead, reserving for ordinal and cardinal exponentiation. This library keeps for the function set, and Ordinal and cardinal are different operations that share one notation ↗ is where the arithmetic exponentiations are distinguished from one another.
-
Degenerate cases. has exactly one element, the empty function, for every , since a function with empty domain has no elements at all. is empty whenever is nonempty, since a function with domain must take a value at each point of , and again has the empty function as its only element.
Depends on
Used by
- A reflexive coequalizer of sets not preserved by Set(ℕ,-) Counterexample
- The functor D(X)=X⊔ X on Set is not covariantly representable Counterexample
- Baire sequence space ℕ^ℕ and its cylinder topology Definition
- Computation alphabets, words, the empty word, and Σ^* Definition
- Initial tapes and machine-relative halting configurations Definition
- The induced R-linear G-module Ind_H^G W as H-covariant functions on G Definition
- The power and the copower of an object by a set Definition
- Trees and their bodies Definition
- Evaluation of functions is dinatural in its argument set Example
- Frobenius reciprocity for group representations without tensor products Example
- Powers and copowers of a set by a set Example
- The distributive and exponential laws of sets are natural isomorphisms Example
- The free word monoid on X represents M mapstoSet(X,U(M)) Example
- The function set B^A represents X mapstoSet(X× A,B) Example
- Coextension of scalars Hom_R(S,M) carries its canonical left S-module structure Lemma
- Discrete sequence spaces are complete in ZF Lemma
- Finite words satisfy the free-monoid universal property Lemma
- For an indexed family (Aᵢ)_i ∈ I the collection of functions f with domain I and f(i) ∈ Aᵢ for every i ∈ I is a set Lemma
- Prescribed-start and starting-point-free serial choice are equivalent in ZF Lemma
- Groups and group homomorphisms form the large locally small category Grp Proposition
- Left modules over a fixed ring and module homomorphisms form the large locally small category R-Mod Proposition
- Posets and monotone maps form the large locally small category Poset Proposition
- Sets and functions form the large locally small category Set Proposition
- Topological spaces and continuous maps form the large locally small category Top Proposition
- Unital rings and unit-preserving ring homomorphisms form the large locally small category Ring Proposition
- Vector spaces over a fixed field and linear maps form the large locally small category Vect_F Proposition
- Currying gives the adjunction -× A⊣(-)^A in Set Theorem
- The end of the function-set functor on a representable is evaluation Theorem
Dependency tree · two levels
10 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- B. Kaya, MATH 320 Set Theory (METU), §2.2 (standard reference, not scraped)
- Function (mathematics) (Wikipedia) (standard reference, not scraped)
- Exponentiation (Wikipedia) (standard reference, not scraped)