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.
The Kuratowski ordered pair
Definition
For sets and , the ordered pair is the set
formed from the unordered pairs and singletons of The unordered pair and the singleton ; three applications of The Axiom of Pairing: produce it. The first coordinate is and the second is .
When the two members coincide, since , and the pair degenerates to .
Remarks
-
Why this set and not another. An ordered pair is required to satisfy one property, that exactly when and ; that is if and only if and , and it is the only thing any later construction uses. Other definitions with the same property exist, and nothing below distinguishes them from this one.
-
The degenerate case is where a careless proof fails. An argument that treats as a set with two distinct members breaks at , and that case has to be handled separately in the proof of the characterising property.
Depends on
Used by
- 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
- Sets A, B, C with (A × B) × C ≠ A × (B × C) Counterexample
- The functor D(X)=X⊔ X on Set is not covariantly representable Counterexample
- 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
- Order embedding and order isomorphism Definition
- Relation, dom R, ran R, fld R, and the specialisations "relation from A to B" and "relation on A" Definition
- The Cartesian product A × B := { z ∈ P(P(A ∪ B)) : ∃ a ∈ A ∃ b ∈ B z = (a,b) } 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 ordered triple (a,b,c) := ((a,b),c) and the iterated products A × B × C := (A × B) × C Definition
- (∅,∅) = {{∅}} and (∅,{∅}) = {{∅},{∅,{∅}}}, with the characterising property checked on them Example
- {∅} × {∅,{∅}} listed in full, together with the inclusion in P(P(A ∪ B)) that makes it a set Example
- ⋃ ⋂ (a,b) = a for all a and b, and ⋃(a,b) = {a,b}, so both coordinates are recovered from the pair as a set Example
- A four-pair relation on {∅,{∅},{∅,{∅}}} with its domain, range, field, inverse, restriction, image and self-composite computed Example
- A tagged disjoint union represents X mapstoSet(A,X)timesSet(B,X) 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
- The distributive and exponential laws of sets are natural isomorphisms 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
- Dependent choice implies countable choice 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 a ∈ A and b ∈ B then (a,b) ∈ P(P(A ∪ B)) Lemma
- If every element of R is an ordered pair, then { a : ∃ b (a,b) ∈ R } and { b : ∃ a (a,b) ∈ R } are sets, both included in ⋃⋃ R Lemma
- Models of the elementary diagram yield elementary embeddings Lemma
- A × (B ∪ C) = (A × B) ∪ (A × C), A × (B ∩ C) = (A × B) ∩ (A × C), A × (B ∖ C) = (A × B) ∖ (A × C), (A ∩ B) × (C ∩ D) = (A × C) ∩ (B × D); A × B = ∅ if and only if A = ∅ or B = ∅; and for nonempty A and B, A × B ⊆ C × D if and only if A ⊆ C and B ⊆ D 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
- (a,b) = (c,d) if and only if a = c and b = d Theorem
Dependency tree · two levels
4 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
- Ordered pair (Wikipedia) (standard reference, not scraped)
- B. Kaya, MATH 320 Set Theory (METU), Def. 1 (standard reference, not scraped)
- C. Wilson, A Brief Introduction to ZFC (Chicago REU 2016), Def. 2.6 (standard reference, not scraped)