From 10027a8277204ed01df2db12c7ba9a16c254882c Mon Sep 17 00:00:00 2001
From: Warren Craft <wdcraft@unm.edu>
Date: Tue, 29 Jul 2025 14:32:55 -0600
Subject: [PATCH 1/9] Establish logic/sets/partitions sub-theory package

Establish the initial logic/sets/partitions sub-theory package, including the Partitions() and PartitionsMembership() classes. The PartitionsMembership() class is not yet developed.
---
 packages/proveit/logic/sets/__init__.py       |  1 +
 .../proveit/logic/sets/_sub_theories_.txt     |  1 +
 .../proveit/logic/sets/partitions/__init__.py |  9 ++
 .../sets/partitions/_brief_description_.txt   |  1 +
 .../logic/sets/partitions/_sub_theories_.txt  |  0
 .../sets/partitions/_theory_nbs_/__init__.py  |  0
 .../sets/partitions/_theory_nbs_/axioms.ipynb | 59 ++++++++++++
 .../sets/partitions/_theory_nbs_/common.ipynb | 59 ++++++++++++
 .../_theory_nbs_/demonstrations.ipynb         | 96 +++++++++++++++++++
 .../partitions/_theory_nbs_/theorems.ipynb    | 59 ++++++++++++
 .../sets/partitions/_theory_nbs_/theory.ipynb | 33 +++++++
 .../logic/sets/partitions/partitions.py       | 41 ++++++++
 .../sets/partitions/partitions_membership.py  | 79 +++++++++++++++
 13 files changed, 438 insertions(+)
 create mode 100644 packages/proveit/logic/sets/partitions/__init__.py
 create mode 100644 packages/proveit/logic/sets/partitions/_brief_description_.txt
 create mode 100644 packages/proveit/logic/sets/partitions/_sub_theories_.txt
 create mode 100644 packages/proveit/logic/sets/partitions/_theory_nbs_/__init__.py
 create mode 100644 packages/proveit/logic/sets/partitions/_theory_nbs_/axioms.ipynb
 create mode 100644 packages/proveit/logic/sets/partitions/_theory_nbs_/common.ipynb
 create mode 100644 packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb
 create mode 100644 packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb
 create mode 100644 packages/proveit/logic/sets/partitions/_theory_nbs_/theory.ipynb
 create mode 100644 packages/proveit/logic/sets/partitions/partitions.py
 create mode 100644 packages/proveit/logic/sets/partitions/partitions_membership.py

diff --git a/packages/proveit/logic/sets/__init__.py b/packages/proveit/logic/sets/__init__.py
index 1229367f29cf..b120119c67cc 100644
--- a/packages/proveit/logic/sets/__init__.py
+++ b/packages/proveit/logic/sets/__init__.py
@@ -15,6 +15,7 @@
 from .cartesian_products import CartProd, CartExp
 from .disjointness import Disjoint, Distinct
 from .cardinality import Card
+from .partitions import Partitions
 from .functions import (Functions, Injections, Surjections, Bijections, 
                         Image, InvImage)
 
diff --git a/packages/proveit/logic/sets/_sub_theories_.txt b/packages/proveit/logic/sets/_sub_theories_.txt
index e660031b52e5..7607e4987a14 100644
--- a/packages/proveit/logic/sets/_sub_theories_.txt
+++ b/packages/proveit/logic/sets/_sub_theories_.txt
@@ -11,3 +11,4 @@ cartesian_products
 disjointness
 cardinality
 functions
+partitions
diff --git a/packages/proveit/logic/sets/partitions/__init__.py b/packages/proveit/logic/sets/partitions/__init__.py
new file mode 100644
index 000000000000..0c803a263f3d
--- /dev/null
+++ b/packages/proveit/logic/sets/partitions/__init__.py
@@ -0,0 +1,9 @@
+from .partitions import Partitions
+
+# KEEP THE FOLLOWING IN __init__.py FOR THEORY PACKAGES.
+#  Make additions above, or add to sys.modules[__name__].__dict__ below.
+# This allows us to import common expression, axioms, and theorems of
+# the theory package directly from the package.
+import sys
+from proveit._core_.theory import TheoryPackage
+sys.modules[__name__] = TheoryPackage(__name__, __file__, locals())
diff --git a/packages/proveit/logic/sets/partitions/_brief_description_.txt b/packages/proveit/logic/sets/partitions/_brief_description_.txt
new file mode 100644
index 000000000000..2de7acdcc439
--- /dev/null
+++ b/packages/proveit/logic/sets/partitions/_brief_description_.txt
@@ -0,0 +1 @@
+Define the class of partitions of a set and related methods.
diff --git a/packages/proveit/logic/sets/partitions/_sub_theories_.txt b/packages/proveit/logic/sets/partitions/_sub_theories_.txt
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/__init__.py b/packages/proveit/logic/sets/partitions/_theory_nbs_/__init__.py
new file mode 100644
index 000000000000..e69de29bb2d1
diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/axioms.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/axioms.ipynb
new file mode 100644
index 000000000000..05d6c9a4c6e4
--- /dev/null
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/axioms.ipynb
@@ -0,0 +1,59 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Axioms for the theory of <a class=\"ProveItLink\" href=\"theory.ipynb\">proveit.logic.sets.partitions</a>\n",
+    "========"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "import proveit\n",
+    "# Prepare this notebook for defining the axioms of a theory:\n",
+    "%axioms_notebook # Keep this at the top following 'import proveit'.\n",
+    "\n",
+    "# from ... import ..."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "%begin axioms"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "%end axioms"
+   ]
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3",
+   "language": "python",
+   "name": "python3"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 0
+}
diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/common.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/common.ipynb
new file mode 100644
index 000000000000..2e52eed01a4c
--- /dev/null
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/common.ipynb
@@ -0,0 +1,59 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Common expressions for the theory of <a class=\"ProveItLink\" href=\"theory.ipynb\">proveit.logic.sets.partitions</a>\n",
+    "========"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "import proveit\n",
+    "# Prepare this notebook for defining the common expressions of a theory:\n",
+    "%common_expressions_notebook # Keep this at the top following 'import proveit'.\n",
+    "\n",
+    "# from ... import ..."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "%begin common"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "%end common"
+   ]
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3",
+   "language": "python",
+   "name": "python3"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 0
+}
diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb
new file mode 100644
index 000000000000..26a9d1bb799b
--- /dev/null
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb
@@ -0,0 +1,96 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Demonstrations for the theory of <a class=\"ProveItLink\" href=\"theory.ipynb\">proveit.logic.sets.partitions</a>\n",
+    "========"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "import proveit\n",
+    "from proveit import P, S\n",
+    "from proveit.logic import InClass, InSet\n",
+    "from proveit.logic.sets import Partitions\n",
+    "%begin demonstrations"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "### Testing of Partition-related Classes & Methods"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "#### Basic Constructions"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Partitions(S) denotes the set of all partitions of set $S$."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "Partitions(S)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "We can claim that $P$ is a partition of set $S$ by claiming that $P$ is in `Partitions(S)`."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InSet(P, Partitions(S))"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "%end demonstrations"
+   ]
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3",
+   "language": "python",
+   "name": "python3"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 0
+}
diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb
new file mode 100644
index 000000000000..e33d7498a28a
--- /dev/null
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb
@@ -0,0 +1,59 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Theorems (or conjectures) for the theory of <a class=\"ProveItLink\" href=\"theory.ipynb\">proveit.logic.sets.partitions</a>\n",
+    "========"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "import proveit\n",
+    "# Prepare this notebook for defining the theorems of a theory:\n",
+    "%theorems_notebook # Keep this at the top following 'import proveit'.\n",
+    "\n",
+    "# from ... import ..."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "%begin theorems"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "%end theorems"
+   ]
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3",
+   "language": "python",
+   "name": "python3"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 0
+}
diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/theory.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/theory.ipynb
new file mode 100644
index 000000000000..62d39423ac69
--- /dev/null
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/theory.ipynb
@@ -0,0 +1,33 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Theory of <a class=\"ProveItLink\" href=\"../../../../_theory_nbs_/theory.ipynb\">proveit</a>.<a class=\"ProveItLink\" href=\"../../../_theory_nbs_/theory.ipynb\">logic</a>.<a class=\"ProveItLink\" href=\"../../_theory_nbs_/theory.ipynb\">sets</a>.partitions\n",
+    "========\n",
+    "\n",
+    "Provide description here."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "import proveit\n",
+    "%theory # toggles between interactive and static modes"
+   ]
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3",
+   "language": "python",
+   "name": "python3"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 0
+}
diff --git a/packages/proveit/logic/sets/partitions/partitions.py b/packages/proveit/logic/sets/partitions/partitions.py
new file mode 100644
index 000000000000..ed67f5df87d6
--- /dev/null
+++ b/packages/proveit/logic/sets/partitions/partitions.py
@@ -0,0 +1,41 @@
+from proveit import Function, Literal
+
+
+class Partitions(Function):
+    '''
+    For a set S, Partitions(S) represents the class of all possible
+    partitions of S. An element P of Partitions(S) is a collection
+    of non-empty subsets S1, S2, ... of S such that the elements
+    of P are all pairwise disjoint and the union S1 U S2 U ...
+    is equal to S. P itself is not required to be finite. When S is
+    finite, Partitions(S) is itself finite and thus a set. When S is
+    infinite, Partitions(S) is a proper class instead of a set.
+    '''
+
+    # the literal string for the Partitions operation
+    _operator_ = Literal(
+        string_format='Partitions',
+        latex_format=r'\textrm{Partitions}',
+        theory=__file__)
+
+    def __init__(self, S, *, styles=None):
+        '''
+        Represent Partions(S), the class of partitions of set S.
+        '''
+        self.set = S
+        Function.__init__(
+                self, Partitions._operator_, S, styles=styles)
+
+    @property
+    def is_proper_class(self):
+        '''
+        For a finite set S, Partitions(S) is a finite set. For an
+        infinite set S, Partitions(S) is infinite. In both cases,
+        Partitions(S) is a set and not a proper class.
+        '''
+        return False
+
+    def membership_object(self, element):
+        from .partitions_membership import PartitionsMembership
+        return PartitionsMembership(element, self)
+    
diff --git a/packages/proveit/logic/sets/partitions/partitions_membership.py b/packages/proveit/logic/sets/partitions/partitions_membership.py
new file mode 100644
index 000000000000..c9b4a389a1c6
--- /dev/null
+++ b/packages/proveit/logic/sets/partitions/partitions_membership.py
@@ -0,0 +1,79 @@
+from proveit import USE_DEFAULTS, equality_prover, prover
+from proveit.logic import SetMembership
+from proveit.numbers import num
+from proveit import m, A, x
+
+
+class PartitionsMembership(SetMembership):
+    '''
+    Defines methods that apply to membership in Partitions(S), the
+    set of partitions of set S. If set S is finite, Partitions(S)
+    is a finite set; if S is infinite, Partitions(S) is infinite.
+    A partition P of a set S is a set of non-empty subsets S1,S2,...
+    of S such that elements of P are mutually disjoint and
+    Union(S1,S2,...) = S.
+    '''
+
+    def __init__(self, element, domain):
+        SetMembership.__init__(self, element, domain)
+
+    # def side_effects(self, judgment):
+    #     '''
+    #     Unfold the enumerated set membership as a side-effect.
+    #     '''
+    #     yield self.unfold
+
+    # @equality_prover('defined', 'define')
+    # def definition(self, **defaults_config):
+    #     '''
+    #     Deduce and return 
+    #         [element in (A union B ...)] = 
+    #         [(element in A) or (element in B) ...]
+    #     where self = (A union B ...).
+    #     '''
+    #     from . import union_def
+    #     element = self.element
+    #     operands = self.domain.operands
+    #     _A = operands
+    #     _m = _A.num_elements()
+    #     return union_def.instantiate(
+    #             {m: _m, x: element, A: _A}, auto_simplify=False)
+
+    # def as_defined(self):
+    #     '''
+    #     From self=[elem in (A U B U ...)], return
+    #     [(element in A) or (element in B) or ...].
+    #     '''
+    #     from proveit.logic import Or, InSet
+    #     element = self.element
+    #     return Or(*self.domain.operands.map_elements(
+    #             lambda subset : InSet(element, subset)))
+
+    # @prover
+    # def unfold(self, **defaults_config):
+    #     '''
+    #     From [element in (A union B ...)], derive and return
+    #     [(element in A) or (element in B) ...],
+    #     where self represents [element in (A union B ...)].
+    #     '''
+    #     from . import membership_unfolding
+    #     element = self.element
+    #     operands = self.domain.operands
+    #     _A = operands
+    #     _m = _A.num_elements()
+    #     return membership_unfolding.instantiate(
+    #         {m: _m, x: element, A: _A}, auto_simplify=False)
+
+    # @prover
+    # def conclude(self, **defaults_config):
+    #     '''
+    #     Called on self = [elem in (A U B U ...)], and knowing or
+    #     assuming [[elem in A] OR [elem in B] OR ...], derive and
+    #     return self.
+    #     '''
+    #     from . import membership_folding
+    #     element = self.element
+    #     operands = self.domain.operands
+    #     _A = operands
+    #     _m = _A.num_elements()
+    #     return membership_folding.instantiate({m: _m, x: element, A: _A})

From e35f79fe5b08995b412a7aa4f7f9297f72e4513b Mon Sep 17 00:00:00 2001
From: Warren Craft <wdcraft@unm.edu>
Date: Tue, 29 Jul 2025 17:52:08 -0600
Subject: [PATCH 2/9] Establish basic axiom, thms, and methods for Partitions &
 PartitionsMembership

Establish the basic axiomatic definition for Partitions(S), some basic theorems defining PartitionsMembership(), and some basic methods for the PartitionsMembership() class. Includes some basic testing in the logic/sets/partitions demmonstrations.ipynb notebook.
---
 .../sets/partitions/_theory_nbs_/axioms.ipynb |  31 +++-
 .../_theory_nbs_/demonstrations.ipynb         |  61 ++++++++
 .../partitions_membership_def/thm_proof.ipynb |  47 ++++++
 .../thm_proof.ipynb                           |  47 ++++++
 .../thm_proof.ipynb                           |  47 ++++++
 .../thm_proof.ipynb                           |  47 ++++++
 .../partitions/_theory_nbs_/theorems.ipynb    |  58 ++++++-
 .../sets/partitions/partitions_membership.py  | 147 +++++++++++-------
 8 files changed, 423 insertions(+), 62 deletions(-)
 create mode 100644 packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partitions_membership_def/thm_proof.ipynb
 create mode 100644 packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partitions_membership_folding/thm_proof.ipynb
 create mode 100644 packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partitions_membership_is_bool/thm_proof.ipynb
 create mode 100644 packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partitions_membership_unfolding/thm_proof.ipynb

diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/axioms.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/axioms.ipynb
index 05d6c9a4c6e4..44b736ee8f61 100644
--- a/packages/proveit/logic/sets/partitions/_theory_nbs_/axioms.ipynb
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/axioms.ipynb
@@ -18,7 +18,9 @@
     "# Prepare this notebook for defining the axioms of a theory:\n",
     "%axioms_notebook # Keep this at the top following 'import proveit'.\n",
     "\n",
-    "# from ... import ..."
+    "from proveit import A, P, S\n",
+    "from proveit.logic import And, Equals, Forall, NotEquals\n",
+    "from proveit.logic.sets import Disjoint, EmptySet, Partitions, PowerSet, SetOfAll, UnionAll"
    ]
   },
   {
@@ -30,12 +32,37 @@
     "%begin axioms"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "A __partition__ $P$ of a set $S$ is a set of non-empty mutually disjoint subsets of $S$ whose union is $S$. This means that a partition $P$ of a set $S$ is a _subset_ of $\\mathcal{P}(S)$, the power set of $S$, and thus $P$ is an _element_ of $\\mathcal{P}(\\mathcal{P}(S))$, and the set of all partitions is a subset of $\\mathcal{P}(\\mathcal{P}(S))$. Using set comprehension, we can formulate this as:\n",
+    "$$\\forall_{S} \\Big[\n",
+    "\\texttt{Partitions}(S) =\n",
+    "\\{P \\,|\\, \\big(\\forall_{A \\in P} (A \\ne \\emptyset)\\big) \\land\n",
+    "\\texttt{Disjoint}(P)                                    \\land\n",
+    "\\big(\\big(\\bigcup\\limits_{A \\in P} A\\big) = S\\big)      \n",
+    "\\}_{P \\in \\mathcal{P}(\\mathcal{P}(S))}\n",
+    "\\Big]$$\n",
+    "and as an axiomatic definition in Prove-It as:"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
-   "source": []
+   "source": [
+    "partitions_def = (\n",
+    "    Forall(S,\n",
+    "    Equals(Partitions(S),\n",
+    "           SetOfAll(P, P,\n",
+    "               conditions = [Forall(A, NotEquals(A, EmptySet), domain = P), Disjoint(P),\n",
+    "                             Equals(UnionAll(A, A, domain = P), S)],\n",
+    "               domain = PowerSet(PowerSet(S)))\n",
+    "    ))\n",
+    ")"
+   ]
   },
   {
    "cell_type": "code",
diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb
index 26a9d1bb799b..d1418c843c2b 100644
--- a/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb
@@ -74,6 +74,67 @@
     "InSet(P, Partitions(S))"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "#### Testing `PartitionsMembership` methods"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InSet(P, Partitions(S)).deduce_in_bool()"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InSet(P, Partitions(S)).definition()"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InSet(P, Partitions(S)).as_defined()"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "in_partitions_means_in_setofall = InSet(P, Partitions(S)).unfold(assumptions = [InSet(P, Partitions(S))])"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "temp_assumption = in_partitions_means_in_setofall.expr"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InSet(P, Partitions(S)).conclude(assumptions = [temp_assumption])"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,
diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partitions_membership_def/thm_proof.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partitions_membership_def/thm_proof.ipynb
new file mode 100644
index 000000000000..b17a0036247b
--- /dev/null
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partitions_membership_def/thm_proof.ipynb
@@ -0,0 +1,47 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Proof of <a class=\"ProveItLink\" href=\"../../../../../../_theory_nbs_/theory.ipynb\">proveit</a>.<a class=\"ProveItLink\" href=\"../../../../../_theory_nbs_/theory.ipynb\">logic</a>.<a class=\"ProveItLink\" href=\"../../../../_theory_nbs_/theory.ipynb\">sets</a>.<a class=\"ProveItLink\" href=\"../../theory.ipynb\">partitions</a>.<a class=\"ProveItLink\" href=\"../../theorems.ipynb#partitions_membership_def\">partitions_membership_def</a> theorem\n",
+    "========"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "import proveit\n",
+    "theory = proveit.Theory() # the theorem's theory"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "%proving partitions_membership_def"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3",
+   "language": "python",
+   "name": "python3"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 0
+}
diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partitions_membership_folding/thm_proof.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partitions_membership_folding/thm_proof.ipynb
new file mode 100644
index 000000000000..050f6353d23a
--- /dev/null
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partitions_membership_folding/thm_proof.ipynb
@@ -0,0 +1,47 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Proof of <a class=\"ProveItLink\" href=\"../../../../../../_theory_nbs_/theory.ipynb\">proveit</a>.<a class=\"ProveItLink\" href=\"../../../../../_theory_nbs_/theory.ipynb\">logic</a>.<a class=\"ProveItLink\" href=\"../../../../_theory_nbs_/theory.ipynb\">sets</a>.<a class=\"ProveItLink\" href=\"../../theory.ipynb\">partitions</a>.<a class=\"ProveItLink\" href=\"../../theorems.ipynb#partitions_membership_folding\">partitions_membership_folding</a> theorem\n",
+    "========"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "import proveit\n",
+    "theory = proveit.Theory() # the theorem's theory"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "%proving partitions_membership_folding"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3",
+   "language": "python",
+   "name": "python3"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 0
+}
diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partitions_membership_is_bool/thm_proof.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partitions_membership_is_bool/thm_proof.ipynb
new file mode 100644
index 000000000000..4ffc2f93d6da
--- /dev/null
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partitions_membership_is_bool/thm_proof.ipynb
@@ -0,0 +1,47 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Proof of <a class=\"ProveItLink\" href=\"../../../../../../_theory_nbs_/theory.ipynb\">proveit</a>.<a class=\"ProveItLink\" href=\"../../../../../_theory_nbs_/theory.ipynb\">logic</a>.<a class=\"ProveItLink\" href=\"../../../../_theory_nbs_/theory.ipynb\">sets</a>.<a class=\"ProveItLink\" href=\"../../theory.ipynb\">partitions</a>.<a class=\"ProveItLink\" href=\"../../theorems.ipynb#partitions_membership_is_bool\">partitions_membership_is_bool</a> theorem\n",
+    "========"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "import proveit\n",
+    "theory = proveit.Theory() # the theorem's theory"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "%proving partitions_membership_is_bool"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3",
+   "language": "python",
+   "name": "python3"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 0
+}
diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partitions_membership_unfolding/thm_proof.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partitions_membership_unfolding/thm_proof.ipynb
new file mode 100644
index 000000000000..d860de4f78e2
--- /dev/null
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partitions_membership_unfolding/thm_proof.ipynb
@@ -0,0 +1,47 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Proof of <a class=\"ProveItLink\" href=\"../../../../../../_theory_nbs_/theory.ipynb\">proveit</a>.<a class=\"ProveItLink\" href=\"../../../../../_theory_nbs_/theory.ipynb\">logic</a>.<a class=\"ProveItLink\" href=\"../../../../_theory_nbs_/theory.ipynb\">sets</a>.<a class=\"ProveItLink\" href=\"../../theory.ipynb\">partitions</a>.<a class=\"ProveItLink\" href=\"../../theorems.ipynb#partitions_membership_unfolding\">partitions_membership_unfolding</a> theorem\n",
+    "========"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "import proveit\n",
+    "theory = proveit.Theory() # the theorem's theory"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "%proving partitions_membership_unfolding"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3",
+   "language": "python",
+   "name": "python3"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 0
+}
diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb
index e33d7498a28a..c0cf999bb8e1 100644
--- a/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb
@@ -18,7 +18,9 @@
     "# Prepare this notebook for defining the theorems of a theory:\n",
     "%theorems_notebook # Keep this at the top following 'import proveit'.\n",
     "\n",
-    "# from ... import ..."
+    "from proveit import A, P, S, X\n",
+    "from proveit.logic import And, Equals, Forall, in_bool, InSet, NotEquals\n",
+    "from proveit.logic.sets import Disjoint, EmptySet, Partitions, PowerSet, SetOfAll, UnionAll"
    ]
   },
   {
@@ -35,7 +37,59 @@
    "execution_count": null,
    "metadata": {},
    "outputs": [],
-   "source": []
+   "source": [
+    "partitions_membership_def = (\n",
+    "    Forall((S, X),\n",
+    "    Equals(InSet(X, Partitions(S)),\n",
+    "           InSet(X, SetOfAll(P, P,\n",
+    "               conditions = [Forall(A, NotEquals(A, EmptySet), domain = P), Disjoint(P),\n",
+    "                             Equals(UnionAll(A, A, domain = P), S)],\n",
+    "               domain = PowerSet(PowerSet(S))))\n",
+    "    ))\n",
+    ")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "partitions_membership_unfolding = (\n",
+    "    Forall((S, X),\n",
+    "    InSet(X, SetOfAll(P, P,\n",
+    "               conditions = [Forall(A, NotEquals(A, EmptySet), domain = P), Disjoint(P),\n",
+    "                             Equals(UnionAll(A, A, domain = P), S)],\n",
+    "               domain = PowerSet(PowerSet(S)))), conditions = [InSet(X, Partitions(S))])\n",
+    ")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "partitions_membership_folding = (\n",
+    "    Forall((S, X),\n",
+    "    InSet(X, Partitions(S)),\n",
+    "    conditions = [InSet(X, SetOfAll(P, P,\n",
+    "               conditions = [Forall(A, NotEquals(A, EmptySet), domain = P), Disjoint(P),\n",
+    "                             Equals(UnionAll(A, A, domain = P), S)],\n",
+    "               domain = PowerSet(PowerSet(S))))])\n",
+    ")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "partitions_membership_is_bool = (\n",
+    "    Forall((S, X), in_bool(InSet(X, Partitions(S))))\n",
+    ")"
+   ]
   },
   {
    "cell_type": "code",
diff --git a/packages/proveit/logic/sets/partitions/partitions_membership.py b/packages/proveit/logic/sets/partitions/partitions_membership.py
index c9b4a389a1c6..8ce718695821 100644
--- a/packages/proveit/logic/sets/partitions/partitions_membership.py
+++ b/packages/proveit/logic/sets/partitions/partitions_membership.py
@@ -1,7 +1,8 @@
 from proveit import USE_DEFAULTS, equality_prover, prover
+from proveit import S, X
 from proveit.logic import SetMembership
-from proveit.numbers import num
-from proveit import m, A, x
+# from proveit.numbers import num
+# from proveit import m, A, x
 
 
 class PartitionsMembership(SetMembership):
@@ -17,63 +18,93 @@ class PartitionsMembership(SetMembership):
     def __init__(self, element, domain):
         SetMembership.__init__(self, element, domain)
 
-    # def side_effects(self, judgment):
-    #     '''
-    #     Unfold the enumerated set membership as a side-effect.
-    #     '''
-    #     yield self.unfold
+    def side_effects(self, judgment):
+        '''
+        No side-effects at this time.
+        '''
+        return
+        yield
 
-    # @equality_prover('defined', 'define')
-    # def definition(self, **defaults_config):
-    #     '''
-    #     Deduce and return 
-    #         [element in (A union B ...)] = 
-    #         [(element in A) or (element in B) ...]
-    #     where self = (A union B ...).
-    #     '''
-    #     from . import union_def
-    #     element = self.element
-    #     operands = self.domain.operands
-    #     _A = operands
-    #     _m = _A.num_elements()
-    #     return union_def.instantiate(
-    #             {m: _m, x: element, A: _A}, auto_simplify=False)
+    @equality_prover('defined', 'define')
+    def definition(self, **defaults_config):
+        '''
+        For self = [element in Partitions(S)], deduce and return the
+        equality:
+            [element in Partitions(S)] = 
+            [element in SetOfAll(P, P, conditions)_{P in Pow(Pow(S))}]
+        where the conditions are:
+            * no element of P is the empty set
+            * the elems of P are all mutually disjoint
+            * the union of all elems of P is S
+        '''
+        from . import partitions_membership_def
+        _X_sub = self.element
+        _S_sub  = self.domain.operand
+        return partitions_membership_def.instantiate(
+                {S: _S_sub, X: _X_sub}, auto_simplify=False)
 
-    # def as_defined(self):
-    #     '''
-    #     From self=[elem in (A U B U ...)], return
-    #     [(element in A) or (element in B) or ...].
-    #     '''
-    #     from proveit.logic import Or, InSet
-    #     element = self.element
-    #     return Or(*self.domain.operands.map_elements(
-    #             lambda subset : InSet(element, subset)))
+    def as_defined(self):
+        '''
+        For self = [element in Partitions(S)], return the expression
+        (NOT a judgment):
+            [element in SetOfAll(P, P, conditions)_{P in Pow(Pow(S))}]
+        where the conditions are:
+            * no element of P is the empty set
+            * the elems of P are all mutually disjoint
+            * the union of all elems of P is S
+        '''
+        from proveit import A, P
+        from proveit.logic import Equals, Forall, InSet, NotEquals
+        from proveit.logic.sets import (
+                Disjoint, EmptySet, PowerSet, SetOfAll, UnionAll)
+        _S = self.domain.operand
+        _X = self.element
+        return InSet(_X,
+               SetOfAll(P, P,
+               conditions = [Forall(A, NotEquals(A, EmptySet), domain = P),
+                             Disjoint(P),
+                             Equals(UnionAll(A, A, domain = P), S)],
+               domain = PowerSet(PowerSet(S))))
 
-    # @prover
-    # def unfold(self, **defaults_config):
-    #     '''
-    #     From [element in (A union B ...)], derive and return
-    #     [(element in A) or (element in B) ...],
-    #     where self represents [element in (A union B ...)].
-    #     '''
-    #     from . import membership_unfolding
-    #     element = self.element
-    #     operands = self.domain.operands
-    #     _A = operands
-    #     _m = _A.num_elements()
-    #     return membership_unfolding.instantiate(
-    #         {m: _m, x: element, A: _A}, auto_simplify=False)
+    @prover
+    def unfold(self, **defaults_config):
+        '''
+        Given self = [element in Partitions(S)] and knowing or
+        assuming self is True, derive and return
+            [element in SetOfAll(P, P, conditions)_{P in Pow(Pow(S))}]
+        where the conditions are:
+            * no element of P is the empty set
+            * the elems of P are all mutually disjoint
+            * the union of all elems of P is S
+        '''
+        from . import partitions_membership_unfolding
+        _S_sub = self.domain.operand
+        _X_sub = self.element
+        return partitions_membership_unfolding.instantiate(
+            {S: _S_sub, X:_X_sub}, auto_simplify=False)
+
+    @prover
+    def conclude(self, **defaults_config):
+        '''
+        Called on self = [elem in Partitions(S)], and knowing or
+        assuming that:
+            [elem in SetOfAll(P, P, conditions)_{P in Pow(Pow(S))}]
+        where the conditions are:
+            * no element of P is the empty set
+            * the elems of P are all mutually disjoint
+            * the union of all elems of P is S,
+        derive and return self.
+        '''
+        from . import partitions_membership_folding
+        _S_sub = self.domain.operand
+        _X_sub = self.element
+        return partitions_membership_folding.instantiate({S: _S_sub, X:_X_sub})
+
+    @prover
+    def deduce_in_bool(self, **defaults_config):
+        from . import partitions_membership_is_bool
+        _S_sub = self.domain.operand
+        _X_sub = self.element
+        return partitions_membership_is_bool.instantiate(
+            {S: _S_sub, X:_X_sub})
 
-    # @prover
-    # def conclude(self, **defaults_config):
-    #     '''
-    #     Called on self = [elem in (A U B U ...)], and knowing or
-    #     assuming [[elem in A] OR [elem in B] OR ...], derive and
-    #     return self.
-    #     '''
-    #     from . import membership_folding
-    #     element = self.element
-    #     operands = self.domain.operands
-    #     _A = operands
-    #     _m = _A.num_elements()
-    #     return membership_folding.instantiate({m: _m, x: element, A: _A})

From dbd048d941253d023fe50c6b5cbd62dd9298c139 Mon Sep 17 00:00:00 2001
From: Warren Craft <wdcraft@unm.edu>
Date: Wed, 30 Jul 2025 11:01:29 -0600
Subject: [PATCH 3/9] Update partitions thms to correctly use Disjoint()

Update the basic logic/sets/partitions theorems to correctly use the Disjoint() predicate (in the previous instantiation, I thought I could call Disjoint(P) where P was a set of sets, but instead Disjoint() takes individual set arguments). For convenience in the future it might be useful to have an alternative like DisjointSets(S) that takes a single set of sets as an argument.
---
 .../logic/sets/partitions/_theory_nbs_/theorems.ipynb | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb
index c0cf999bb8e1..0d81073f307d 100644
--- a/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb
@@ -18,7 +18,7 @@
     "# Prepare this notebook for defining the theorems of a theory:\n",
     "%theorems_notebook # Keep this at the top following 'import proveit'.\n",
     "\n",
-    "from proveit import A, P, S, X\n",
+    "from proveit import A, B, P, S, X\n",
     "from proveit.logic import And, Equals, Forall, in_bool, InSet, NotEquals\n",
     "from proveit.logic.sets import Disjoint, EmptySet, Partitions, PowerSet, SetOfAll, UnionAll"
    ]
@@ -42,7 +42,8 @@
     "    Forall((S, X),\n",
     "    Equals(InSet(X, Partitions(S)),\n",
     "           InSet(X, SetOfAll(P, P,\n",
-    "               conditions = [Forall(A, NotEquals(A, EmptySet), domain = P), Disjoint(P),\n",
+    "               conditions = [Forall(A, NotEquals(A, EmptySet), domain = P),\n",
+    "                             Forall((A,B), Disjoint(A, B), domain = P),\n",
     "                             Equals(UnionAll(A, A, domain = P), S)],\n",
     "               domain = PowerSet(PowerSet(S))))\n",
     "    ))\n",
@@ -58,7 +59,8 @@
     "partitions_membership_unfolding = (\n",
     "    Forall((S, X),\n",
     "    InSet(X, SetOfAll(P, P,\n",
-    "               conditions = [Forall(A, NotEquals(A, EmptySet), domain = P), Disjoint(P),\n",
+    "               conditions = [Forall(A, NotEquals(A, EmptySet), domain = P),\n",
+    "                             Forall((A,B), Disjoint(A, B), domain = P),\n",
     "                             Equals(UnionAll(A, A, domain = P), S)],\n",
     "               domain = PowerSet(PowerSet(S)))), conditions = [InSet(X, Partitions(S))])\n",
     ")"
@@ -74,7 +76,8 @@
     "    Forall((S, X),\n",
     "    InSet(X, Partitions(S)),\n",
     "    conditions = [InSet(X, SetOfAll(P, P,\n",
-    "               conditions = [Forall(A, NotEquals(A, EmptySet), domain = P), Disjoint(P),\n",
+    "               conditions = [Forall(A, NotEquals(A, EmptySet), domain = P),\n",
+    "                             Forall((A,B), Disjoint(A, B), domain = P),\n",
     "                             Equals(UnionAll(A, A, domain = P), S)],\n",
     "               domain = PowerSet(PowerSet(S))))])\n",
     ")"

From 9bd00902aad40b9f4e76ff06ba56525b61b146b7 Mon Sep 17 00:00:00 2001
From: Warren Craft <wdcraft@unm.edu>
Date: Fri, 1 Aug 2025 09:44:12 -0500
Subject: [PATCH 4/9] Update sets/partitions/ demos nb

Update the logic/sets/partitions/ demonstrations notebook with some efforts to use the Partitions(S) concept in a simple example, mostly failing the demonstration because the partition concept is challenging to use due to the multiple conditions required (non-empty subsets, mutually disjoint, whose union is the original set).
---
 .../_theory_nbs_/demonstrations.ipynb         | 144 ++++++++++++++++++
 1 file changed, 144 insertions(+)

diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb
index d1418c843c2b..6a15029358f5 100644
--- a/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb
@@ -135,6 +135,150 @@
     "InSet(P, Partitions(S)).conclude(assumptions = [temp_assumption])"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "#### Utilizing the Partitions(S) Concept"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "The sets $A = \\{1, 2, 3, 4, 5\\}$ and $B = \\{6, 7, 8, 9, 10\\}$ form a partition of the set $C = \\{1, 2, \\ldots, 10\\}$. Can we prove that $\\{A, B\\} \\in \\texttt{Partitions}(C)$?"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from proveit import x, A, B, C\n",
+    "from proveit.logic import Equals, Exists, Forall, Not, NotEquals, NotExists\n",
+    "from proveit.logic.sets import Disjoint, EmptySet, Set, Union\n",
+    "from proveit.numbers import one, five, six, Interval, num"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "A, B, C, partition_set = [\n",
+    "    Interval(one, five), Interval(six, num(10)), Interval(one, num(10)), Set(Interval(one, five), Interval(six, num(10)))]"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "partition_set"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "Disjoint(A, B).conclude()"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "In the definition of a partition, we need all partitioning sets to be mutually disjoint, which will not be easy to confirm, as illustrated here:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "try:\n",
+    "    Forall((A, B), Disjoint(A, B), domain = partition_set).prove()\n",
+    "except Exception as the_exception:\n",
+    "    print(f\"Exception: {the_exception}\")"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "How do we prove that $A$ and $B$ are each _not_ the empty set? It turns out that it's not straighforward despite the fact that we have, and can “do”, the following:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from proveit.logic.sets import nothing_is_in_empty\n",
+    "nothing_is_in_empty"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "nothing_is_in_empty.inner_expr().instance_expr.unfold_not_in()"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "one_is_not_in_emptyset = nothing_is_in_empty.instantiate({x: one})"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "one_is_in_A = InSet(one, A).prove()"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "The fact that $1 \\in \\{1, 2, 3, 4, 5\\}$ but $1 \\notin \\emptyset$ does not, however, allow Prove-It to automatically conclude that $\\{1, 2, 3, 4, 5\\}$ is not the empty set."
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "So, we'll put the non-equality with the EmptySet into the assumptions … but this is still a nightmare:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "try:\n",
+    "    InSet(partition_set, Partitions(C)).conclude(\n",
+    "    assumptions = [NotEquals(A, EmptySet), NotEquals(B, EmptySet), Equals(Union(A, B), C)])\n",
+    "except Exception as the_exception:\n",
+    "    print(f\"Exception: {the_exception}\")"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,

From 723fa5fdac609df442c85da1e7ecd801ceb00eea Mon Sep 17 00:00:00 2001
From: Warren Craft <wdcraft@unm.edu>
Date: Mon, 4 Aug 2025 11:28:22 -0500
Subject: [PATCH 5/9] Update partitions with corrected use of Disjoint

Update the logic/sets/partitions sub-theory package with correction to the use of Disjoint(), changing the condition Disjoint(P) to a Disjoint(A,B) for all A, B in P. Also reorder the conditions in the axiomatic def and related theorems to put the union condition first (per request by WW).
---
 .../sets/partitions/_theory_nbs_/axioms.ipynb  |  7 ++++---
 .../partitions/_theory_nbs_/theorems.ipynb     | 18 +++++++++---------
 .../sets/partitions/partitions_membership.py   |  8 ++++----
 3 files changed, 17 insertions(+), 16 deletions(-)

diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/axioms.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/axioms.ipynb
index 44b736ee8f61..cbfcb6f66e8b 100644
--- a/packages/proveit/logic/sets/partitions/_theory_nbs_/axioms.ipynb
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/axioms.ipynb
@@ -18,7 +18,7 @@
     "# Prepare this notebook for defining the axioms of a theory:\n",
     "%axioms_notebook # Keep this at the top following 'import proveit'.\n",
     "\n",
-    "from proveit import A, P, S\n",
+    "from proveit import A, B, P, S\n",
     "from proveit.logic import And, Equals, Forall, NotEquals\n",
     "from proveit.logic.sets import Disjoint, EmptySet, Partitions, PowerSet, SetOfAll, UnionAll"
    ]
@@ -57,8 +57,9 @@
     "    Forall(S,\n",
     "    Equals(Partitions(S),\n",
     "           SetOfAll(P, P,\n",
-    "               conditions = [Forall(A, NotEquals(A, EmptySet), domain = P), Disjoint(P),\n",
-    "                             Equals(UnionAll(A, A, domain = P), S)],\n",
+    "               conditions = [Equals(UnionAll(A, A, domain = P), S),\n",
+    "                             Forall(A, NotEquals(A, EmptySet), domain = P),\n",
+    "                             Forall((A, B), Disjoint(A, B), domain = P)],\n",
     "               domain = PowerSet(PowerSet(S)))\n",
     "    ))\n",
     ")"
diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb
index 0d81073f307d..28f3940e09af 100644
--- a/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb
@@ -42,9 +42,9 @@
     "    Forall((S, X),\n",
     "    Equals(InSet(X, Partitions(S)),\n",
     "           InSet(X, SetOfAll(P, P,\n",
-    "               conditions = [Forall(A, NotEquals(A, EmptySet), domain = P),\n",
-    "                             Forall((A,B), Disjoint(A, B), domain = P),\n",
-    "                             Equals(UnionAll(A, A, domain = P), S)],\n",
+    "               conditions = [Equals(UnionAll(A, A, domain = P), S),\n",
+    "                             Forall(A, NotEquals(A, EmptySet), domain = P),\n",
+    "                             Forall((A,B), Disjoint(A, B), domain = P)],\n",
     "               domain = PowerSet(PowerSet(S))))\n",
     "    ))\n",
     ")"
@@ -59,9 +59,9 @@
     "partitions_membership_unfolding = (\n",
     "    Forall((S, X),\n",
     "    InSet(X, SetOfAll(P, P,\n",
-    "               conditions = [Forall(A, NotEquals(A, EmptySet), domain = P),\n",
-    "                             Forall((A,B), Disjoint(A, B), domain = P),\n",
-    "                             Equals(UnionAll(A, A, domain = P), S)],\n",
+    "               conditions = [Equals(UnionAll(A, A, domain = P), S),\n",
+    "                             Forall(A, NotEquals(A, EmptySet), domain = P),\n",
+    "                             Forall((A,B), Disjoint(A, B), domain = P)],\n",
     "               domain = PowerSet(PowerSet(S)))), conditions = [InSet(X, Partitions(S))])\n",
     ")"
    ]
@@ -76,9 +76,9 @@
     "    Forall((S, X),\n",
     "    InSet(X, Partitions(S)),\n",
     "    conditions = [InSet(X, SetOfAll(P, P,\n",
-    "               conditions = [Forall(A, NotEquals(A, EmptySet), domain = P),\n",
-    "                             Forall((A,B), Disjoint(A, B), domain = P),\n",
-    "                             Equals(UnionAll(A, A, domain = P), S)],\n",
+    "               conditions = [Equals(UnionAll(A, A, domain = P), S),\n",
+    "                             Forall(A, NotEquals(A, EmptySet), domain = P),\n",
+    "                             Forall((A,B), Disjoint(A, B), domain = P)],\n",
     "               domain = PowerSet(PowerSet(S))))])\n",
     ")"
    ]
diff --git a/packages/proveit/logic/sets/partitions/partitions_membership.py b/packages/proveit/logic/sets/partitions/partitions_membership.py
index 8ce718695821..841b1ca2eb16 100644
--- a/packages/proveit/logic/sets/partitions/partitions_membership.py
+++ b/packages/proveit/logic/sets/partitions/partitions_membership.py
@@ -53,7 +53,7 @@ def as_defined(self):
             * the elems of P are all mutually disjoint
             * the union of all elems of P is S
         '''
-        from proveit import A, P
+        from proveit import A, B, P
         from proveit.logic import Equals, Forall, InSet, NotEquals
         from proveit.logic.sets import (
                 Disjoint, EmptySet, PowerSet, SetOfAll, UnionAll)
@@ -61,9 +61,9 @@ def as_defined(self):
         _X = self.element
         return InSet(_X,
                SetOfAll(P, P,
-               conditions = [Forall(A, NotEquals(A, EmptySet), domain = P),
-                             Disjoint(P),
-                             Equals(UnionAll(A, A, domain = P), S)],
+               conditions = [Equals(UnionAll(A, A, domain = P), S),
+                             Forall(A, NotEquals(A, EmptySet), domain = P),
+                             Forall((A, B), Disjoint(A, B), domain = P)],
                domain = PowerSet(PowerSet(S))))
 
     @prover

From 3d06761803223fcc35d4368f31a798e77ec85324 Mon Sep 17 00:00:00 2001
From: Warren Craft <wdcraft@unm.edu>
Date: Mon, 4 Aug 2025 17:17:22 -0500
Subject: [PATCH 6/9] Add PartitionsMembership side-effect

Add a call to self.unfold for PartitionsMembership.side_effcts().
---
 .../logic/sets/partitions/partitions_membership.py        | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/packages/proveit/logic/sets/partitions/partitions_membership.py b/packages/proveit/logic/sets/partitions/partitions_membership.py
index 841b1ca2eb16..4f7b073ddd1d 100644
--- a/packages/proveit/logic/sets/partitions/partitions_membership.py
+++ b/packages/proveit/logic/sets/partitions/partitions_membership.py
@@ -20,10 +20,12 @@ def __init__(self, element, domain):
 
     def side_effects(self, judgment):
         '''
-        No side-effects at this time.
+        Main side effect is to unfold the basic definition of
+        memberhip in the set of partitions. If P is an element of
+        Partitions(S), then P is a set of non-empty subsets of S
+        whose union is S.
         '''
-        return
-        yield
+        yield self.unfold
 
     @equality_prover('defined', 'define')
     def definition(self, **defaults_config):

From 729ad030f0dd34f30f3a66ada9095cb97d575078 Mon Sep 17 00:00:00 2001
From: Warren Craft <wdcraft@unm.edu>
Date: Mon, 4 Aug 2025 17:18:36 -0500
Subject: [PATCH 7/9] Update logic/sets/partitions demonstrations nb for recent
 changes

Update the logic/sets/partitions demonstrations.ipynb notebook for recent changes and commits to partitions-related material.
---
 .../_theory_nbs_/demonstrations.ipynb         | 115 ++++--------------
 1 file changed, 27 insertions(+), 88 deletions(-)

diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb
index 6a15029358f5..4cda491aa913 100644
--- a/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb
@@ -15,19 +15,13 @@
    "outputs": [],
    "source": [
     "import proveit\n",
-    "from proveit import P, S\n",
-    "from proveit.logic import InClass, InSet\n",
-    "from proveit.logic.sets import Partitions\n",
+    "from proveit import x, A, B, C, P, S, defaults\n",
+    "from proveit.logic import Equals, Forall, InClass, InSet, NotEquals\n",
+    "from proveit.logic.sets import Disjoint, EmptySet, Partitions, PowerSet, Set, SetOfAll, UnionAll\n",
+    "from proveit.numbers import one, five, six, num, Interval\n",
     "%begin demonstrations"
    ]
   },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "metadata": {},
-   "outputs": [],
-   "source": []
-  },
   {
    "cell_type": "markdown",
    "metadata": {},
@@ -139,26 +133,12 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "#### Utilizing the Partitions(S) Concept"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "metadata": {},
-   "source": [
-    "The sets $A = \\{1, 2, 3, 4, 5\\}$ and $B = \\{6, 7, 8, 9, 10\\}$ form a partition of the set $C = \\{1, 2, \\ldots, 10\\}$. Can we prove that $\\{A, B\\} \\in \\texttt{Partitions}(C)$?"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "from proveit import x, A, B, C\n",
-    "from proveit.logic import Equals, Exists, Forall, Not, NotEquals, NotExists\n",
-    "from proveit.logic.sets import Disjoint, EmptySet, Set, Union\n",
-    "from proveit.numbers import one, five, six, Interval, num"
+    "#### Checking Side-Effects of `Partitions(S)` Membership\n",
+    "\n",
+    "If $P \\in \\texttt{Partitions}(S)$, then we know that:\n",
+    "- $\\bigcup\\limits_{A \\in P} A = S$\n",
+    "- $\\forall_{A \\in P}\\big(A \\ne \\emptyset\\big)$\n",
+    "- $\\forall_{A, B \\in P}\\big(\\texttt{disjoint}(A, B)\\big)$\n"
    ]
   },
   {
@@ -167,8 +147,7 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "A, B, C, partition_set = [\n",
-    "    Interval(one, five), Interval(six, num(10)), Interval(one, num(10)), Set(Interval(one, five), Interval(six, num(10)))]"
+    "defaults.assumptions = [InSet(P, Partitions(S))]"
    ]
   },
   {
@@ -177,7 +156,11 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "partition_set"
+    "InSet(P, SetOfAll(P, P,\n",
+    "                  conditions = [Equals(UnionAll(A, A, domain = P), S),\n",
+    "                                Forall(A, NotEquals(A, EmptySet), domain = P),\n",
+    "                                Forall((A, B), Disjoint(A, B), domain = P)],\n",
+    "                  domain = PowerSet(PowerSet(S)))).prove()"
    ]
   },
   {
@@ -186,33 +169,25 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "Disjoint(A, B).conclude()"
+    "defaults.assumptions = []"
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "In the definition of a partition, we need all partitioning sets to be mutually disjoint, which will not be easy to confirm, as illustrated here:"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "try:\n",
-    "    Forall((A, B), Disjoint(A, B), domain = partition_set).prove()\n",
-    "except Exception as the_exception:\n",
-    "    print(f\"Exception: {the_exception}\")"
+    "#### Utilizing the Partitions(S) Concept?"
    ]
   },
   {
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "How do we prove that $A$ and $B$ are each _not_ the empty set? It turns out that it's not straighforward despite the fact that we have, and can “do”, the following:"
+    "At the time of this writing (August 2025), the Partitions concept is difficult to use at the level of proofs, because we still lack some infrastructure development to support the establishment of the required conditions that the elements of the supposed partition all consist of non-empty mutually-disjoint subsets of the original set whose union gives the original set.\n",
+    "\n",
+    "For example, the sets $A = \\{1, 2, 3, 4, 5\\}$ and $B = \\{6, 7, 8, 9, 10\\}$ form a partition of the set $C = \\{1, 2, \\ldots, 10\\}$. Can we prove that $\\{A, B\\} \\in \\texttt{Partitions}(C)$? Not at this time. It's difficult to even prove that $A$ and $B$ are each not equal to the empty set. And though we can pretty easily prove that $A$ and $B$ are disjoint, due to prior development of the enumerated set Set() class, it is then still difficult to convert that to a proof that $\\forall_{A, B \\in P}\\big(\\texttt{disjoint}(A, B)\\big)$ for $P = \\{A, B\\}$.\n",
+    "\n",
+    "Nevertheless, it could and will be useful to be able to posit or assumer that some set of sets, say $P$, is a partition of some other set, say $S$, allowing us to then conclude that elements of $P$ are non-empty mutually-disjoint subsets of $S$ whose union gives $S$. The accessibility of such conclusions will depend on the development in the SetOfAll class."
    ]
   },
   {
@@ -221,26 +196,8 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "from proveit.logic.sets import nothing_is_in_empty\n",
-    "nothing_is_in_empty"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "nothing_is_in_empty.inner_expr().instance_expr.unfold_not_in()"
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "one_is_not_in_emptyset = nothing_is_in_empty.instantiate({x: one})"
+    "A, B, C, partition_set = [\n",
+    "    Interval(one, five), Interval(six, num(10)), Interval(one, num(10)), Set(Interval(one, five), Interval(six, num(10)))]"
    ]
   },
   {
@@ -249,21 +206,7 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "one_is_in_A = InSet(one, A).prove()"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "metadata": {},
-   "source": [
-    "The fact that $1 \\in \\{1, 2, 3, 4, 5\\}$ but $1 \\notin \\emptyset$ does not, however, allow Prove-It to automatically conclude that $\\{1, 2, 3, 4, 5\\}$ is not the empty set."
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "metadata": {},
-   "source": [
-    "So, we'll put the non-equality with the EmptySet into the assumptions … but this is still a nightmare:"
+    "partition_set"
    ]
   },
   {
@@ -272,11 +215,7 @@
    "metadata": {},
    "outputs": [],
    "source": [
-    "try:\n",
-    "    InSet(partition_set, Partitions(C)).conclude(\n",
-    "    assumptions = [NotEquals(A, EmptySet), NotEquals(B, EmptySet), Equals(Union(A, B), C)])\n",
-    "except Exception as the_exception:\n",
-    "    print(f\"Exception: {the_exception}\")"
+    "Disjoint(A, B).conclude()"
    ]
   },
   {

From 5fed9ab2b184672d5863e2c1b6b1f3a8d663a73a Mon Sep 17 00:00:00 2001
From: Warren Craft <wdcraft@unm.edu>
Date: Mon, 4 Aug 2025 17:20:57 -0500
Subject: [PATCH 8/9] Fix typo in comments in partitions demonstrations.ipynb

Fix a typo in some comments in the logic/sets/partitions demonstrations.ipynb notebook.
---
 .../logic/sets/partitions/_theory_nbs_/demonstrations.ipynb     | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb
index 4cda491aa913..a73181c6c429 100644
--- a/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/demonstrations.ipynb
@@ -187,7 +187,7 @@
     "\n",
     "For example, the sets $A = \\{1, 2, 3, 4, 5\\}$ and $B = \\{6, 7, 8, 9, 10\\}$ form a partition of the set $C = \\{1, 2, \\ldots, 10\\}$. Can we prove that $\\{A, B\\} \\in \\texttt{Partitions}(C)$? Not at this time. It's difficult to even prove that $A$ and $B$ are each not equal to the empty set. And though we can pretty easily prove that $A$ and $B$ are disjoint, due to prior development of the enumerated set Set() class, it is then still difficult to convert that to a proof that $\\forall_{A, B \\in P}\\big(\\texttt{disjoint}(A, B)\\big)$ for $P = \\{A, B\\}$.\n",
     "\n",
-    "Nevertheless, it could and will be useful to be able to posit or assumer that some set of sets, say $P$, is a partition of some other set, say $S$, allowing us to then conclude that elements of $P$ are non-empty mutually-disjoint subsets of $S$ whose union gives $S$. The accessibility of such conclusions will depend on the development in the SetOfAll class."
+    "Nevertheless, it could and will be useful to be able to posit or assume that some set of sets, say $P$, is a partition of some other set, say $S$, allowing us to then conclude that elements of $P$ are non-empty mutually-disjoint subsets of $S$ whose union gives $S$. The accessibility of such conclusions will depend on the development in the SetOfAll class."
    ]
   },
   {

From e87d102997a8ec567cc1e9e94ae3f414d6ececa0 Mon Sep 17 00:00:00 2001
From: Warren Craft <wdcraft@unm.edu>
Date: Mon, 4 Aug 2025 17:36:45 -0500
Subject: [PATCH 9/9] Add one thm to logic/sets/partitions sub-theory pkg

Add one thm to logic/sets/partitions sub-theory pkg: partition_elements_are_subsets. Not yet clear how to incorporate this into a method but seems a reasonably important theorem to have: if x is an element of a partition X, where X is in Partitions(S), then x must be a subset of S.
---
 .../thm_proof.ipynb                           | 47 +++++++++++++++++++
 .../partitions/_theory_nbs_/theorems.ipynb    | 14 +++++-
 2 files changed, 59 insertions(+), 2 deletions(-)
 create mode 100644 packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partition_elements_are_subsets/thm_proof.ipynb

diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partition_elements_are_subsets/thm_proof.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partition_elements_are_subsets/thm_proof.ipynb
new file mode 100644
index 000000000000..f981489b15c7
--- /dev/null
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/proofs/partition_elements_are_subsets/thm_proof.ipynb
@@ -0,0 +1,47 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Proof of <a class=\"ProveItLink\" href=\"../../../../../../_theory_nbs_/theory.ipynb\">proveit</a>.<a class=\"ProveItLink\" href=\"../../../../../_theory_nbs_/theory.ipynb\">logic</a>.<a class=\"ProveItLink\" href=\"../../../../_theory_nbs_/theory.ipynb\">sets</a>.<a class=\"ProveItLink\" href=\"../../theory.ipynb\">partitions</a>.<a class=\"ProveItLink\" href=\"../../theorems.ipynb#partition_elements_are_subsets\">partition_elements_are_subsets</a> theorem\n",
+    "========"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "import proveit\n",
+    "theory = proveit.Theory() # the theorem's theory"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "%proving partition_elements_are_subsets"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3",
+   "language": "python",
+   "name": "python3"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 0
+}
diff --git a/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb b/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb
index 28f3940e09af..0306330fd3ce 100644
--- a/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb
+++ b/packages/proveit/logic/sets/partitions/_theory_nbs_/theorems.ipynb
@@ -18,9 +18,10 @@
     "# Prepare this notebook for defining the theorems of a theory:\n",
     "%theorems_notebook # Keep this at the top following 'import proveit'.\n",
     "\n",
-    "from proveit import A, B, P, S, X\n",
+    "from proveit import x, A, B, P, S, X\n",
     "from proveit.logic import And, Equals, Forall, in_bool, InSet, NotEquals\n",
-    "from proveit.logic.sets import Disjoint, EmptySet, Partitions, PowerSet, SetOfAll, UnionAll"
+    "from proveit.logic.sets import (Disjoint, EmptySet, Partitions, PowerSet,\n",
+    "        SetOfAll, SubsetEq, UnionAll)"
    ]
   },
   {
@@ -83,6 +84,15 @@
     ")"
    ]
   },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "partition_elements_are_subsets = Forall((x, X, S), SubsetEq(x, S), conditions = [InSet(X, Partitions(S)), InSet(x, X)])"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,
