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 image and the preimage of a set under a relation
Definition
Let be a relation (Relation, , , , and the specialisations "relation from to " and "relation on ") and let and be sets. The image of under and the preimage of under are
sets by The Axiom Schema of Separation: for each formula , applied inside and respectively. Thus holds if and only if for some , and holds if and only if for some (The Kuratowski ordered pair ).
The notation is consistent: applying the first clause to the inverse relation of The inverse relation , the composite , and the restriction gives , which has exactly the elements just described, since says and .
Remarks
-
The bracket is not an application. is the set of things related to something in ; it is written with square brackets precisely so that it is never confused with a value , which for a general relation does not exist. Even for a function, and mean different things, and only the bracket form is used here.
-
Image and range. Taking gives , and taking gives , since no lies in .
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 Axiom Schema of Separation: for each formula $\varphi$, $\forall \bar p\,\forall x\,\exists y\,\forall z\,(z \in y \leftrightarrow (z \in x \wedge \varphi(z,\bar p)))$
- The inverse relation $R^{-1}$, the composite $S \circ R$, and the restriction $R \restriction A$
- The Kuratowski ordered pair $(a,b) := \{\{a\},\{a,b\}\}$
Used by
- 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
- Injection, surjection, bijection Definition
- A four-pair relation on {∅,{∅},{∅,{∅}}} with its domain, range, field, inverse, restriction, image and self-composite computed Example
- A two-to-one function on a four-element set, its kernel, the quotient, and the canonical factorisation computed explicitly Example
- Open-set and closed-set functors on Topᵒᵖ are naturally isomorphic by complements Example
- Singletons define a natural transformation from the identity functor on sets to the covariant power-set functor Example
- 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
- 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
- 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
- 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
- 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
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 17 results over 10 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. 7, Def. 8 and Lemma 2 (standard reference, not scraped)
- Image (mathematics) (Wikipedia) (standard reference, not scraped)
- Binary relation (Wikipedia) (standard reference, not scraped)