Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-06 (claude-opus-5)
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.

For f:A→Bf : A \to B and T,U⊆BT, U \subseteq B: f−1[T∪U]=f−1[T]∪f−1[U]f^{-1}[T \cup U] = f^{-1}[T] \cup f^{-1}[U], f−1[T∩U]=f−1[T]∩f−1[U]f^{-1}[T \cap U] = f^{-1}[T] \cap f^{-1}[U], f−1[T∖U]=f−1[T]∖f−1[U]f^{-1}[T \setminus U] = f^{-1}[T] \setminus f^{-1}[U], and f−1[B∖T]=A∖f−1[T]f^{-1}[B \setminus T] = A \setminus f^{-1}[T]

Statement

Let f:A→Bf : A \to B and let T,U⊆BT, U \subseteq B. Then

f−1[T∪U]=f−1[T]∪f−1[U],f−1[T∩U]=f−1[T]∩f−1[U],f^{-1}[T \cup U] = f^{-1}[T] \cup f^{-1}[U], \qquad f^{-1}[T \cap U] = f^{-1}[T] \cap f^{-1}[U],

f−1[T∖U]=f−1[T]∖f−1[U],f−1[B∖T]=A∖f−1[T].f^{-1}[T \setminus U] = f^{-1}[T] \setminus f^{-1}[U], \qquad f^{-1}[B \setminus T] = A \setminus f^{-1}[T].

Facts & Assumptions

Given: a function f:A→Bf : A \to B and subsets T,UT, U of BB.

[L1]

a∈R−1[B]a \in R^{-1}[B] holds if and only if (a,b)∈R(a,b) \in R for some b∈Bb \in B (The image R[A]R[A] and the preimage R−1[B]R^{-1}[B] of a set under a relation).

[L2]

We write f:A→Bf : A \to B, and say ff is a function from AA to BB, when ff is a function with dom⁡f=A\operatorname{dom} f = A and ran⁡f⊆B\operatorname{ran} f \subseteq B (A function is a relation ff with (a,b)∈f(a,b) \in f and (a,c)∈f(a,c) \in f implying b=cb = c; f:A→Bf : A \to B, the value f(a)f(a), domain and codomain).

[L3]

z∈a∪bz \in a \cup b holds if and only if z∈az \in a or z∈bz \in b (⋃∅=∅\bigcup \varnothing = \varnothing, ⋃{a}=a\bigcup \{a\} = a, ⋃{a,b}=a∪b\bigcup \{a,b\} = a \cup b, ⋂{a}=a\bigcap \{a\} = a, and ⋂{a,b}=a∩b\bigcap \{a,b\} = a \cap b).

[L4]

z∈a∩bz \in a \cap b holds if and only if z∈az \in a and z∈bz \in b (⋃∅=∅\bigcup \varnothing = \varnothing, ⋃{a}=a\bigcup \{a\} = a, ⋃{a,b}=a∪b\bigcup \{a,b\} = a \cup b, ⋂{a}=a\bigcap \{a\} = a, and ⋂{a,b}=a∩b\bigcap \{a,b\} = a \cap b).

[L5]

z∈a∖bz \in a \setminus b holds exactly when z∈az \in a and z∉bz \notin b (The difference a∖ba \setminus b, the symmetric difference a△ba \triangle b, and the complement X∖aX \setminus a relative to a set XX).

[L6]

If every zz satisfies z∈xz \in x if and only if z∈yz \in y, then x=yx = y (The Axiom of Extensionality: ∀x ∀y (∀z (z∈x↔z∈y)→x=y)\forall x\,\forall y\,(\forall z\,(z \in x \leftrightarrow z \in y) \to x = y)).

[L7]

dom⁡R:={ a:∃b (a,b)∈R }\operatorname{dom} R := \{\, a : \exists b\ (a,b) \in R \,\} (Relation, dom⁡R\operatorname{dom} R, ran⁡R\operatorname{ran} R, fld⁡R\operatorname{fld} R, and the specialisations "relation from AA to BB" and "relation on AA").

[L8]

x⊆yx \subseteq y means that every element of xx is an element of yy (Subset x⊆yx \subseteq y, proper subset x⊊yx \subsetneq y, and the separation notation { z∈x:φ(z) }\{\, z \in x : \varphi(z) \,\}).

Proof

technique · direct
1.1

Membership criterion: for any S⊆BS \subseteq B, a∈f−1[S]a \in f^{-1}[S] holds exactly when a∈Aa \in A and f(a)∈Sf(a) \in S. Indeed a∈f−1[S]a \in f^{-1}[S] says (a,b)∈f(a,b) \in f for some b∈Sb \in S, and (a,b)∈f(a,b) \in f says a∈dom⁡f=Aa \in \operatorname{dom} f = A and b=f(a)b = f(a).

L1L2L7L8
2.1

First identity: a∈f−1[T∪U]a \in f^{-1}[T \cup U] exactly when a∈Aa \in A and f(a)∈Tf(a) \in T or f(a)∈Uf(a) \in U, which is exactly a∈f−1[T]a \in f^{-1}[T] or a∈f−1[U]a \in f^{-1}[U].

L3L6step 1.1
2.2

Second identity: a∈f−1[T∩U]a \in f^{-1}[T \cap U] exactly when a∈Aa \in A and f(a)f(a) lies in both TT and UU, which is exactly a∈f−1[T]a \in f^{-1}[T] and a∈f−1[U]a \in f^{-1}[U].

L4L6step 1.1
2.3

Third identity: a∈f−1[T∖U]a \in f^{-1}[T \setminus U] exactly when a∈Aa \in A, f(a)∈Tf(a) \in T and f(a)∉Uf(a) \notin U; the last two conditions say a∈f−1[T]a \in f^{-1}[T] and a∉f−1[U]a \notin f^{-1}[U], since for a∈Aa \in A membership in f−1[U]f^{-1}[U] is exactly f(a)∈Uf(a) \in U.

L5L6step 1.1
2.4

Fourth identity: a∈f−1[B∖T]a \in f^{-1}[B \setminus T] exactly when a∈Aa \in A, f(a)∈Bf(a) \in B and f(a)∉Tf(a) \notin T; the condition f(a)∈Bf(a) \in B is automatic because ran⁡f⊆B\operatorname{ran} f \subseteq B, so this says a∈Aa \in A and a∉f−1[T]a \notin f^{-1}[T].

L2L5L6step 1.1
3.1

The four identities are established, which is the statement.

step 2.1step 2.2step 2.3step 2.4∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 25 results over 12 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