Alphabeta MathHow 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.
Functions and are equal if and only if and for every in that common domain
Statement
Let and be functions. Then if and only if and for every .
Facts & Assumptions
Given: functions and .
A function is a relation such that and imply (A function is a relation with and implying ; , the value , domain and codomain).
if and only if and ( if and only if and ).
If every satisfies if and only if , then (The Axiom of Extensionality: ).
Proof
From left to right: if then the two sets have the same elements, so the defining conditions for the domain and for the value at a point are the same for both.
From right to left: assume and for every in that set. Let . Then is an ordered pair with and ; hence and , so . The same argument with and exchanged gives the reverse inclusion, so the two sets have the same elements.
Both implications hold, which is the statement.
Depends on
- A function is a relation $f$ with $(a,b) \in f$ and $(a,c) \in f$ implying $b = c$; $f : A \to B$, the value $f(a)$, domain and codomain
- The Axiom of Extensionality: $\forall x\,\forall y\,(\forall z\,(z \in x \leftrightarrow z \in y) \to x = y)$
- Relation, $\operatorname{dom} R$, $\operatorname{ran} R$, $\operatorname{fld} R$, and the specialisations "relation from $A$ to $B$" and "relation on $A$"
- The Kuratowski ordered pair $(a,b) := \{\{a\},\{a,b\}\}$
- $(a,b) = (c,d)$ if and only if $a = c$ and $b = d$
Used by
- For I = {∅,{∅}} with A_∅ = A and A_{∅} = B, the map f ↦ (f(∅), f({∅})) is a bijection ∏_i ∈ I Aᵢ → 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
- 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
- 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: 17 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), §2.2 (standard reference, not scraped)
- Function (mathematics) (Wikipedia) (standard reference, not scraped)
- C. Wilson, A Brief Introduction to ZFC (Chicago REU 2016), Def. 2.10 (standard reference, not scraped)