A subset B is a statement, sets are equal by double containment, and powerset(A) is a set

[Rafael-SOWNet]

Item 4 of the docket on #1409 (Sullivan and Mackey §§3.3–3.5), the first half: the statements and constructions on sets that the chapter's exercises are written in. Its rows are the tests.

A subset B — also A ⊆ B, and B superset A / B ⊇ A for the same node — is Entity.Set.Subsetf, a Statement at the level of in: the relation between two sets that in is between an element and a set, and the book's first point about the two ({1, 2} subset {1, 2, 3} is True, {1, 2} in {1, 2, 3} is False). Decided in SetOperators.Subset, in order:

route	example
the shapes outright: same node, empty on the left	A subset A, {} subset A
the set algebra, for symbols standing for sets (Lemma 3.9.2's shape)	A /\ B subset A, A subset A \/ B, A \ B subset A, A \/ B subset C iff both, powerset(A) subset powerset(B) iff A subset B
a set builder whose predicate the solver settles to a list is that list	{ x in RR : x^2 = 5 } subset ZZ → False
member by member for a listed set	{sqrt(3), -pi, 8.2} subset QQ → False
the chain ZZ+ ⊂ ZZ* ⊂ ZZ ⊂ QQ ⊂ RR ⊂ CC, BB beside it	QQ subset ZZ → False
intervals against intervals and against the chain	(0; 1) subset [0; 1], [0; 1] subset QQ → False, [3; 3] subset ZZ
sub \ super where the operators evaluate it	empty is yes, a listed member is no
the definition, forall x in A : x in B, put to the quantifier decision (#1421) with the membership spelled as the comparison it is — an interval's two bounds, a listed set's equalities, an integer set inside the one x ranges over (x in ZZ+ over ZZ is x >= 1), a set builder's declared membership and predicate	{ x in ZZ : x >= 1 } subset ZZ+ → True, ZZ+ subset { x in ZZ : x >= 1 } → True

NaN with a number or a truth value on a side.

= between two sets is decided by double containment, the book's definition: { x in ZZ : x >= 1 } = ZZ+ is True, [0; 1] = [0; 2] is False. Two things this corrects on the way: {1, 2} = {1, 2, 3} was { True, False } and {1, x} = {1, 2} was { True, False, x = 1, x = 2 } — the comparison distributed over the members of each side — and are False and the statement left as written.

powerset(A), Entity.Set.Powersetf: listed for a finite argument (FiniteSet.GetPowerSet crashed on the empty set with an IndexOutOfRangeException; powerset({}) is { {} }, one member), and for an infinite one an object whose membership is the subset test: {1, 3, 7} in powerset(ZZ+) is True, ZZ+ in powerset(ZZ) is True. card(powerset(A)) is 2^card(A), and card counts a listed set whose members are listed sets (card({1, {}}) is 2, §3.3.7).

MathS.Sets.Subset, MathS.Sets.PowerSet, Entity.SubsetOf, Entity.PowerSet; subset, superset, powerset are keywords now. Syntax.md, BREAKING-CHANGES.md (rows measured on a v2.5.0 build), PublicApi.txt regenerated, parser regenerated and post-processed.

SubsetTest: §3.4.1's six claims, the chain, intervals, the algebra on symbols, §3.4.5 Try 3's eleven statements about one set (with two distinct numbers for the book's x and ♥, since a symbol x might be 4), Ex 3.4.3–4 and Try 1–2's power sets, §3.3.3's equalities. Full suite 12110 passed, 0 failed; benchmark gate PASSED (SimplifyHard 173,260,088 B, +1.0% on the recorded baseline: the set-equality decision is on the evaluation path, and two distinct sets compared by = now go through the subset decision both ways).

Not in this PR, next: complement relative to a universe, indexed unions and intersections, tuples and Cartesian products (the second half of item 4), then relations (item 5).

Part of #1409.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura