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.
A function is a relation with and implying ; , the value , domain and codomain
Definition
A function is a relation such that and imply ; "relation" is as in Relation, , , , and the specialisations "relation from to " and "relation on ".
For there is such a , and by the condition just stated there is only one; denotes that unique , so that holds if and only if and ( if and only if and ).
We write , and say is a function from to , when is a function with and (Subset , proper subset , and the separation notation ); is the domain of and is a codomain for . Equivalently with (The Cartesian product , The Kuratowski ordered pair ).
Remarks
-
The codomain belongs to the declaration, not to the set. A function is a set of ordered pairs, and that set determines its domain and its range but not a codomain: the same satisfies for every containing . So being onto is a property of the declaration rather than of , while being one-to-one is a property of alone. This convention is what makes a function for every at once.
-
Total on its domain by construction. There is no partial function here: if then is not defined, and a function has equal to exactly, not merely included in it.
Depends on
- Relation, $\operatorname{dom} R$, $\operatorname{ran} R$, $\operatorname{fld} R$, and the specialisations "relation from $A$ to $B$" and "relation on $A$"
- The Cartesian product $A \times B := \{\, z \in \mathcal{P}(\mathcal{P}(A \cup B)) : \exists a \in A\ \exists b \in B\ z = (a,b) \,\}$
- The Kuratowski ordered pair $(a,b) := \{\{a\},\{a,b\}\}$
- $(a,b) = (c,d)$ if and only if $a = c$ and $b = d$
- Subset $x \subseteq y$, proper subset $x \subsetneq y$, and the separation notation $\{\, z \in x : \varphi(z) \,\}$
Used by
- For a nonempty index set I: B ∩ ⋃_i ∈ I Aᵢ = ⋃_i ∈ I (B ∩ Aᵢ), B ∪ ⋂_i ∈ I Aᵢ = ⋂_i ∈ I (B ∪ Aᵢ), X ∖ ⋃_i ∈ I Aᵢ = ⋂_i ∈ I (X ∖ Aᵢ), and X ∖ ⋂_i ∈ I Aᵢ = ⋃_i ∈ I (X ∖ Aᵢ) Corollary
- For f : A → B with A ≠ ∅: f is injective if and only if there is g : B → A with g ∘ f = Δ_A; for A = ∅ the empty function is injective and has a left inverse if and only if B = ∅ Corollary
- For f : A → B: S ⊆ f⁻¹[f[S]] for every S ⊆ A, with equality for every such S if and only if f is injective; and f[f⁻¹[T]] = T ∩ f[A] for every T ⊆ B, so equality with T holds for every such T if and only if f is surjective Corollary
- A function f and sets S, T with f[S ∩ T] ⊊ f[S] ∩ f[T] Counterexample
- An indexed family (Aᵢ)_i ∈ I is a function with domain I; {Aᵢ : i ∈ I} is its range Definition
- Binary operation on a set; associativity, commutativity, and a subset closed under the operation Definition
- Category, object, morphism, domain, codomain, identity, composition, and hom-collection Definition
- Choice function Definition
- Column-multilinear, alternating, normalized and antisymmetric functions on square matrices over a commutative ring Definition
- Equivalence relation, equivalence class, and the quotient set A/∼ Definition
- Equivariant maps and isomorphisms of group actions Definition
- Finite rectangular matrices over a commutative ring, their entries, rows and columns Definition
- Injection, surjection, bijection Definition
- Peano system Definition
- The product ∏_i ∈ I Aᵢ := { f : I → ⋃_i ∈ I Aᵢ ∣ f(i) ∈ Aᵢ for every i ∈ I } Definition
- The set B^A of all functions A → B Definition
- ∅ is a relation on every set, is the unique equivalence relation on ∅, is a function ∅ → B for every B, is a bijection ∅ → ∅, and is not a surjection ∅ → {∅} Example
- A two-to-one function on a four-element set, its kernel, the quotient, and the canonical factorisation computed explicitly Example
- For any indexed family the product ∏_i ∈ I P(Xᵢ) contains the constant function with value ∅, and ∏_i ∈ I {i} has exactly one element Example
- FALSE: assuming ZF is consistent, ZF proves that every surjection f : A → B has a right inverse g : B → A with f ∘ g = Δ_B False statement
- For a function f : A → B the relation ker f := { (a,a') ∈ A × A : f(a) = f(a') } is an equivalence relation on A 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
- For I = {∅,{∅}} with A_∅ = A and A_{∅} = B, the map f ↦ (f(∅), f({∅})) is a bijection ∏_i ∈ I Aᵢ → A × B Lemma
- For sets A and B the collection of all functions A → B is a set, being a subset of P(A × B) Lemma
- Functions f and g are equal if and only if dom f = dom g and f(x) = g(x) for every x in that common domain Lemma
- If f and g are functions then g ∘ f is a function with domain f⁻¹[dom g] and (g ∘ f)(x) = g(f(x)) there; Δ_A is a function with Δ_A(a) = a; and f ∘ Δ_A = f = Δ_B ∘ f for f : A → B Lemma
- ∏_i ∈ ∅ Aᵢ = {∅}; if Aⱼ = ∅ for some j ∈ I then ∏_i ∈ I Aᵢ = ∅; and for I = {j} the evaluation f ↦ f(j) is a bijection ∏_i ∈ I Aᵢ → Aⱼ Proposition
- For f : A → B and g : B → C: if both are injective so is g ∘ f; if both are surjective so is g ∘ f; if g ∘ f is injective so is f; and if g ∘ f is surjective so is g Proposition
- For f : A → B and S, T ⊆ A: f[S ∪ T] = f[S] ∪ f[T], f[S ∩ T] ⊆ f[S] ∩ f[T] and f[S] ∖ f[T] ⊆ f[S ∖ T]; both inclusions are equalities for all S and T if and only if f is injective Proposition
- Sets and functions form the large locally small category Set Proposition
- Every function f : A → B factors as f = ι ∘ bar f ∘ π with π : A → A/ker f the surjective quotient map, bar f : A/ker f → f[A] the bijection [a] ↦ f(a), and ι : f[A] → B the inclusion injection; bar f is the only function making the factorisation hold Theorem
- f : A → B is a bijection if and only if there is a function g : B → A with g ∘ f = Δ_A and f ∘ g = Δ_B; such a g is unique, equals the inverse relation f⁻¹, and is itself a bijection Theorem
- For f : A → B and T, U ⊆ B: f⁻¹[T ∪ U] = f⁻¹[T] ∪ f⁻¹[U], f⁻¹[T ∩ U] = f⁻¹[T] ∩ f⁻¹[U], f⁻¹[T ∖ U] = f⁻¹[T] ∖ f⁻¹[U], and f⁻¹[B ∖ T] = A ∖ f⁻¹[T] Theorem
- Let ∼ be an equivalence relation on A with quotient map π : A → A/∼, and let f : A → B. There is a function g : A/∼ → B with g ∘ π = f if and only if a ∼ a' implies f(a) = f(a'); and such a g is then unique Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 18 results over 8 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
- B. Kaya, MATH 320 Set Theory (METU), Def. 15 to Def. 17 (standard reference, not scraped)
- C. Wilson, A Brief Introduction to ZFC (Chicago REU 2016), Def. 2.10 (standard reference, not scraped)
- Function (mathematics) (Wikipedia) (standard reference, not scraped)