Set operations: union, intersection, difference and complement in an explicit universe

Goal and scope

Universe U={1,2,3,4,5,6,7,8}, A={2,4,6,8}, B={3,4,5,6}. Compute A∪B, A∩B, A∖B, B∖A, U∖A and U∖B element by element; show A∖B≠B∖A; show that the complement of A changes when the universe is U′={1,2,3,4,5,6,7,8,9,10}; prove U∖(A∪B)=(U∖A)∩(U∖B) for arbitrary sets and check it on this example; and use A∪B=A∪(B∖A) to explain why the union has 6 elements, not 8.

Treats finite sets in one explicit universe (MKO assumptions a1 and a2). The operations are defined by membership conditions and computed element by element; De Morgan's law is proved by a general argument, and the example only checks it. It does not bind Lean declarations such as Set.mem_union, and does not change the canonical MKO or its English edition.

Givens and symbols

• set_operations_def
• set_extensionality
• subset_def
• finite_set_listing
• finite_counting_basics
• de_morgan_logic

• G1 — Universe U={1,2,3,4,5,6,7,8} (MKO assumption a2: the universe is stated before any complement is used).
• G2 — A={2,4,6,8} and B={3,4,5,6}.
• G3 — A second universe for comparison: U′={1,2,3,4,5,6,7,8,9,10}.

• U,\ U' — two explicit universes
• A\cup B — union: in at least one of the sets
• A\cap B — intersection: in both sets
• A\setminus B — difference: in A but not in B
• U\setminus A — the complement of A relative to U
• |X| — the number of elements of a finite set X
• (T,F) — a row of the membership table: x∈A true, x∈B false

Rules and sources

• set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
• de_morgan_logic · prerequisite — De Morgan's laws for logic: ¬(P∧Q) ⇔ ¬P∨¬Q and ¬(P∨Q) ⇔ ¬P∧¬Q.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• mko_set_ops · cited — For sets A and B in one domain, the union contains elements belonging to at least one set, the intersection contains elements belonging to both, and A∖B contains elements belonging to A but not B. A complement must be relative to an explicit universe U and is written U∖A. · mko-set-operations
• finite_set_listing · prerequisite — Listed sets: x belongs to a finite set given by a list exactly when x equals one of the listed objects; the order and repetitions of the list do not change the set, for example {4,4,6}={4,6}.
• L_ops_in_U · lemma — If A⊆U and B⊆U, then A∪B, A∩B, A∖B and B∖A are subsets of U.
• L_de_morgan_set · lemma — For any sets U, A, B: U∖(A∪B)=(U∖A)∩(U∖B).
• L_union_split · lemma — For any sets A, B: A∪B=A∪(B∖A), and A∩(B∖A)=∅.

Main derivation

\text{a universe and two sets}

U=\{1,2,3,4,5,6,7,8\},\ A=\{2,4,6,8\},\ B=\{3,4,5,6\}

A=\{2,4,6,8\},\ B=\{3,4,5,6\},\ U=\{1,2,3,4,5,6,7,8\}

A\subseteq U,\ B\subseteq U

A\subseteq U,\ B\subseteq U

A\cup B,\ A\cap B,\ A\setminus B,\ B\setminus A\subseteq U

x\in U

1{:}(F,F),\ 2{:}(T,F),\ 3{:}(F,T),\ 4{:}(T,T),\ 5{:}(F,T),\ 6{:}(T,T),\ 7{:}(F,F),\ 8{:}(T,F)

A\cup B

\{2,3,4,5,6,8\}

A\cap B

\{4,6\}

A\setminus B

\{2,8\}

B\setminus A

\{3,5\}

A\setminus B=\{2,8\},\ B\setminus A=\{3,5\}

A\setminus B\neq B\setminus A

U\setminus A,\ U\setminus B

U\setminus A=\{1,3,5,7\},\ U\setminus B=\{1,2,7,8\}

U'\setminus A

U'\setminus A=\{1,3,5,7,9,10\}\neq U\setminus A

U\setminus(A\cup B)

(U\setminus A)\cap(U\setminus B)

U\setminus\{2,3,4,5,6,8\},\quad \{1,3,5,7\}\cap\{1,2,7,8\}

\{1,7\}=\{1,7\}

A\cup B

A\cup(B\setminus A)\ \text{with}\ A\cap(B\setminus A)=\varnothing

|A\cup B|=|A\cup(B\setminus A)|

|A\cup B|=|A|+|B\setminus A|=4+2=6

\text{membership table of }U

A\cup B=\{2,3,4,5,6,8\},\ A\cap B=\{4,6\},\ A\setminus B=\{2,8\},\ B\setminus A=\{3,5\},\ U\setminus A=\{1,3,5,7\},\ U\setminus B=\{1,2,7,8\}

Substeps and lemmas

x\in A\cup B

x\in U

x\in A\cap B\ \lor\ x\in A\setminus B\ \lor\ x\in B\setminus A

x\in U

x\in U\setminus(A\cup B)

x\in U\land\neg(x\in A\lor x\in B)

x\in U\land\neg(x\in A\lor x\in B)

x\in U\land x\notin A\land x\notin B

x\in U\land x\notin A\land x\notin B

x\in(U\setminus A)\cap(U\setminus B)

x\in A\lor(x\in B\land x\notin A)

x\in A\lor x\in B

x\in A\cap(B\setminus A)

A\cap(B\setminus A)=\varnothing

Reverse audits

• S16 · sufficient_goal_reduction · S05, S06, S07, S08, S09, S10, S11, S13, S15, and_intro_elim — Goal G is the conjunction of the problem's conclusions; each conjunct is obtained forwards from the givens by the listed steps, and this step only forms the conjunction; G is never used as a premise.
• S15 · premise_audit · S14, finite_counting_basics — The addition rule applies only to disjoint sets, so S14.2's A∩(B∖A)=∅ is needed first; adding the sizes of A and B directly is not allowed, because A∩B≠∅.
• S14.2 · premise_audit · set_operations_def, contradiction — Only the two unfoldings and the contradiction are needed; it is not claimed that A∩B=∅ (here A∩B={4,6}).
• S14.1 · inverse_equivalence · case_analysis, set_operations_def — In each case the two sides are equivalent, and the cases are exhaustive, so the equivalence holds both ways.
• S14 · inverse_equivalence · L_union_split — The lemma gives an equality of sets, so the step holds both ways; disjointness is given separately by S14.2.
• S13 · premise_audit · S05, S10, S12, set_operations_def — This is a check on one example and can be recomputed independently; it does not replace the general proof in S12, and one example could not prove De Morgan's law.
• S12.3 · inverse_equivalence · and_intro_elim, set_operations_def, set_extensionality — Regrouping and duplicating conjuncts are two-way; for each x both sides are true or false together, so the sets are equal.
• S12.2 · inverse_equivalence · de_morgan_logic — De Morgan's law is itself an equivalence, so the step holds both ways.
• S12.1 · inverse_equivalence · set_operations_def — Both unfoldings of definitions are two-way.
• S12 · inverse_equivalence · L_de_morgan_set — The lemma proves an equality of sets, obtained from an element-wise two-way equivalence.
• S11 · premise_audit · G3, set_operations_def, set_extensionality — U′ must be explicit; the single witness 9 is enough to refute equality of the two complements.
• S10 · inverse_equivalence · mko_set_ops, set_operations_def, set_extensionality — U∖A is decided element by element by its membership condition, compared both ways; no object outside U belongs to U∖A.
• S09 · premise_audit · S07, S08, set_extensionality — One element in only one of the sets is enough to refute equality. It is not claimed that A∖B and B∖A differ for all sets: when A=B both are ∅.
• S08 · inverse_equivalence · set_operations_def, set_extensionality, S03 — As in S05, membership is compared element by element in both directions.
• S07 · inverse_equivalence · set_operations_def, set_extensionality, S03 — As in S05, membership is compared element by element in both directions.
• S06 · inverse_equivalence · set_operations_def, set_extensionality, S03 — As in S05, membership is compared element by element in both directions.
• S05 · inverse_equivalence · set_operations_def, set_extensionality, S03 — Both sides decide membership the same way for every object: row by row in U, and outside U neither contains it (S03); by set equality the step holds both ways.
• S04 · premise_audit · finite_set_listing, S03 — Each row can be rechecked against the lists; the table covers all of U, so no element is missed.
• S03.2 · premise_audit · set_operations_def, and_intro_elim, subset_def — It only extracts one conjunct; no converse is claimed (elements of U need not lie in these sets).
• S03.1 · premise_audit · set_operations_def, subset_def, case_analysis — The two cases cover every possibility of the 'or'; each case uses one of the inclusion hypotheses.
• S03 · premise_audit · S02, L_ops_in_U — It needs A⊆U and B⊆U (S02); if A had an element outside U, testing only U would miss elements of the union.
• S02 · premise_audit · subset_def, finite_set_listing — This is a complete enumeration, not a sample: every element of A and of B is checked. The converse U⊆A is not claimed (1∈U but 1∉A).
• S01 · premise_audit · G1, G2, def_intro, finite_set_listing — This step only records the data and derives no new fact; the universe is explicit, as assumption a2 requires.

Error controls and negative controls

Swapping union and intersection

The MKO names the mistake of swapping union and intersection. Union corresponds to 'or' (in at least one set), intersection to 'and' (in both). Here 2∈A∪B but 2∉A∩B; the union has 6 elements and the intersection only 2. To catch the error, go back to the membership table and check whether the rule reads 'at least one T' or 'both T'.

Difference has a direction

The MKO warns that A∖B and B∖A usually differ. Here A∖B={2,8} while B∖A={3,5} (S07 to S09), and they are even disjoint. They are equal only in special cases (for example A=B, when both are ∅).

A complement needs a universe first

The MKO warns against listing a complement without a specified universe. The same A={2,4,6,8} has complement {1,3,5,7} in U but {1,3,5,7,9,10} in U′ (S10, S11). So one must write U∖A and list U first.

• A∖B=B∖A → reject — 2∈A∖B but 2∉B∖A (S09).
• A∩B={2,3,4,5,6,8} → reject — That is the union; 2∉B, so 2∉A∩B, and the correct answer is {4,6}.
• A∪B has |A|+|B|=8 elements → reject — 4 and 6 belong to both sets but count once; |A∪B|=6 (S15).
• Without naming a universe, the complement of A={2,4,6,8} is {1,3,5,7} → reject — In U′ the complement is {1,3,5,7,9,10} (S11); the complement depends on the universe.
• U∖(A∪B)=(U∖A)∪(U∖B) → reject — The right side is {1,2,3,5,7,8} and the left side is {1,7}; the correct De Morgan law has an intersection on the right (S12).

Result and limitations

In the universe U={1,2,3,4,5,6,7,8}: A∪B={2,3,4,5,6,8}, A∩B={4,6}, A∖B={2,8}, B∖A={3,5}, U∖A={1,3,5,7}, U∖B={1,2,7,8}. A∖B≠B∖A; with the universe U′ the complement of A becomes {1,3,5,7,9,10}; U∖(A∪B)=(U∖A)∩(U∖B) holds for all sets, and both sides are {1,7} here; |A∪B|=|A|+|B∖A|=6.

• The count checks in S10 and S11 use that U is the disjoint union of A and U∖A when A⊆U; this follows by the same argument as S14, and no separate lemma is stated here.

Verification and source binding

8 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: c42753a14041612b07055d8ace7c5c9df4c243cd4ab72e79efd18921fc2f0b46
• original source SHA-256: c42753a14041612b07055d8ace7c5c9df4c243cd4ab72e79efd18921fc2f0b46
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)