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.
Relation, , , , and the specialisations "relation from to " and "relation on "
Definition
A relation is a set every element of which is an ordered pair (The Kuratowski ordered pair ). We write for .
By If every element of is an ordered pair, then and are sets, both included in the following two classes are sets, so the notation is legitimate:
the domain and the range of . The field of is (The union of a set, and the binary union ).
is a relation from to when (The Cartesian product , Subset , proper subset , and the separation notation ), and a relation on when .
Remarks
-
Domain and range are intrinsic; the sets and are not. A relation determines its own domain and range, but it is a relation from to for many different and : any containing and any containing will do. That is the content of Every relation satisfies , and is a relation from to if and only if and , and it is the same distinction that makes a codomain part of the declaration rather than of the set in A function is a relation with and implying ; , the value , domain and codomain.
-
The empty set is a relation. It has no elements, so the requirement that every element be an ordered pair holds vacuously, and . It is a relation on every set.
Depends on
- If every element of $R$ is an ordered pair, then $\{\, a : \exists b\ (a,b) \in R \,\}$ and $\{\, b : \exists a\ (a,b) \in R \,\}$ are sets, both included in $\bigcup\bigcup R$
- The Kuratowski ordered pair $(a,b) := \{\{a\},\{a,b\}\}$
- 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 union $\bigcup x$ of a set, and the binary union $a \cup b := \bigcup \{a,b\}$
- 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
- A symmetric and transitive relation on a two-element set that is not reflexive on it Counterexample
- Relations R and S on a two-element set with S ∘ R ≠ R ∘ S Counterexample
- ⋃_i ∈ I Aᵢ := ⋃ {Aᵢ : i ∈ I}, and ⋂_i ∈ I Aᵢ := ⋂ {Aᵢ : i ∈ I} for I ≠ ∅ Definition
- A function is a relation f with (a,b) ∈ f and (a,c) ∈ f implying b = c; f : A → B, the value f(a), domain and codomain Definition
- An indexed family (Aᵢ)_i ∈ I is a function with domain I; {Aᵢ : i ∈ I} is its range Definition
- Equivalence relation, equivalence class, and the quotient set A/∼ Definition
- One-step derivation and finite derivation in a context-free grammar Definition
- Reflexive, irreflexive, symmetric, asymmetric, antisymmetric, transitive, and connex relations on a set Definition
- The identity relation Δ_A = { (a,b) ∈ A × A : a = b } and the membership relation ∈_A = { (a,b) ∈ A × A : a ∈ b } Definition
- The image R[A] and the preimage R⁻¹[B] of a set under a relation Definition
- The inverse relation R⁻¹, the composite S ∘ R, and the restriction R ↾ A Definition
- The serial-relation Dependent Choice principle over ZF 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 four-pair relation on {∅,{∅},{∅,{∅}}} with its domain, range, field, inverse, restriction, image and self-composite computed Example
- A two-cell partition of a three-element set, the equivalence relation it induces listed pair by pair, and the quotient set recovered from it 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: a symmetric and transitive relation on a set A is reflexive on A, so reflexivity is redundant in the definition of an equivalence relation False statement
- Every relation R satisfies R ⊆ dom R × ran R, and R is a relation from A to B if and only if dom R ⊆ A and ran R ⊆ B Lemma
- 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 relations R and S and a set A, the collections { (b,a) : (a,b) ∈ R }, { (a,c) : ∃ b ((a,b) ∈ R ∧ (b,c) ∈ S) } and { (a,b) ∈ R : a ∈ A } are sets 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
- R[A ∪ B] = R[A] ∪ R[B], R[A ∩ B] ⊆ R[A] ∩ R[B], R[A] ∖ R[B] ⊆ R[A ∖ B], A ⊆ B implies R[A] ⊆ R[B], and (S ∘ R)[A] = S[R[A]] Proposition
- T ∘ (S ∘ R) = (T ∘ S) ∘ R, (S ∘ R)⁻¹ = R⁻¹ ∘ S⁻¹, (R⁻¹)⁻¹ = R, dom(R⁻¹) = ran R, and Δ_B ∘ R = R = R ∘ Δ_A for a relation R from A to B Proposition
- Every function f : A → B factors as f = ι ∘ f̄ ∘ π with π : A → A/ker f the surjective quotient map, f̄ : A/ker f → f[A] the bijection [a] ↦ f(a), and ι : f[A] → B the inclusion injection; 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
- On a set A, R ↦ R ∖ Δ_A and S ↦ S ∪ Δ_A are mutually inverse bijections between the partial orders on A and the irreflexive, transitive relations on A; R ∖ Δ_A is the strict order of R, and every irreflexive transitive relation is asymmetric Theorem
Dependency tree · two levels
13 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), Def. 6 and Def. 11 (standard reference, not scraped)
- Binary relation (Wikipedia) (standard reference, not scraped)
- C. Wilson, A Brief Introduction to ZFC (Chicago REU 2016), Def. 2.9 (standard reference, not scraped)