From 629cf96f3d18b79988d92cd99fea1d98f0e20170 Mon Sep 17 00:00:00 2001
From: Warren Craft <wdcraft@unm.edu>
Date: Thu, 10 Jul 2025 10:53:13 -0600
Subject: [PATCH 1/4] Update sets/functions_def axiom

Update the functions_def axiom in numbers/sets/functions sub-theory package to more carefully specify functions with domain A and codomain B instead of functions that take A to B but might also have elements outside of A in their domain.
---
 .../proveit/logic/sets/functions/_theory_nbs_/axioms.ipynb   | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/packages/proveit/logic/sets/functions/_theory_nbs_/axioms.ipynb b/packages/proveit/logic/sets/functions/_theory_nbs_/axioms.ipynb
index 6bbc9385e62b..82089ebb803e 100644
--- a/packages/proveit/logic/sets/functions/_theory_nbs_/axioms.ipynb
+++ b/packages/proveit/logic/sets/functions/_theory_nbs_/axioms.ipynb
@@ -19,7 +19,7 @@
     "%axioms_notebook # Keep this at the top following 'import proveit'.\n",
     "\n",
     "from proveit import f, x, A, B, fx\n",
-    "from proveit.logic import Forall, Equals, InSet\n",
+    "from proveit.logic import And, Equals, FALSE, Forall, InSet, NotInSet\n",
     "from proveit.logic.sets import Functions"
    ]
   },
@@ -47,7 +47,8 @@
    "source": [
     "functions_def = Forall(\n",
     "    (f, A, B), Equals(InSet(f, Functions(A, B)),\n",
-    "                      Forall(x, InSet(fx, B), domain=A)))"
+    "                      And(Forall(x, InSet(fx, B), domain=A),\n",
+    "    Forall(x, Equals(fx, FALSE), conditions = [NotInSet(x, A)]))))"
    ]
   },
   {

From d19c016820ac511a909a25d234454ef7e61be51a Mon Sep 17 00:00:00 2001
From: Warren Craft <wdcraft@unm.edu>
Date: Sun, 13 Jul 2025 16:16:51 -0600
Subject: [PATCH 2/4] Add UNDEF literal

Add UNDEF literal, a common expression labeled as 'undefined' in logic/sets/functions, most immediately for use in the expression of function-related expressions where the function is not defined for some set of inputs. This is then used in an update to the functions_def axiomatic definition of sets/functions and related theorems.
---
 .../logic/sets/functions/_theory_nbs_/common.ipynb  | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/packages/proveit/logic/sets/functions/_theory_nbs_/common.ipynb b/packages/proveit/logic/sets/functions/_theory_nbs_/common.ipynb
index 8058fa985890..50981aceb5a5 100644
--- a/packages/proveit/logic/sets/functions/_theory_nbs_/common.ipynb
+++ b/packages/proveit/logic/sets/functions/_theory_nbs_/common.ipynb
@@ -18,7 +18,7 @@
     "# 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 ..."
+    "from proveit import Literal"
    ]
   },
   {
@@ -30,12 +30,21 @@
     "%begin common"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "An undefined “UNDEF” literal, for use in defining function values for inputs outside the given domain of the function."
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
-   "source": []
+   "source": [
+    "undefined = Literal('UNDEF', r'\\textrm{UNDEF}')"
+   ]
   },
   {
    "cell_type": "code",

From 20a459cbfaf4958dae4f01332e315e520242a740 Mon Sep 17 00:00:00 2001
From: Warren Craft <wdcraft@unm.edu>
Date: Sun, 13 Jul 2025 16:19:44 -0600
Subject: [PATCH 3/4] Update functions_def axiom and establish Restriction()
 class

Update the functions_def axiom in logic/sets/functions to utilize the UNDEF literal for undefined function outputs and establish the Restriction() class in logic/sets/functions along with related axiomatic definition, a related theorem, and some entries in the logic/sets/functions demonstrations notebook.
---
 packages/proveit/logic/sets/__init__.py       |   4 +-
 .../proveit/logic/sets/functions/__init__.py  |   1 +
 .../sets/functions/_theory_nbs_/axioms.ipynb  |  36 +++++-
 .../_theory_nbs_/demonstrations.ipynb         | 106 +++++++++++++++++-
 .../restriction_membership/thm_proof.ipynb    |  47 ++++++++
 .../functions/_theory_nbs_/theorems.ipynb     |  23 +++-
 .../logic/sets/functions/restriction.py       |  37 ++++++
 7 files changed, 243 insertions(+), 11 deletions(-)
 create mode 100644 packages/proveit/logic/sets/functions/_theory_nbs_/proofs/restriction_membership/thm_proof.ipynb
 create mode 100644 packages/proveit/logic/sets/functions/restriction.py

diff --git a/packages/proveit/logic/sets/__init__.py b/packages/proveit/logic/sets/__init__.py
index 1229367f29cf..203c5458e035 100644
--- a/packages/proveit/logic/sets/__init__.py
+++ b/packages/proveit/logic/sets/__init__.py
@@ -15,8 +15,8 @@
 from .cartesian_products import CartProd, CartExp
 from .disjointness import Disjoint, Distinct
 from .cardinality import Card
-from .functions import (Functions, Injections, Surjections, Bijections, 
-                        Image, InvImage)
+from .functions import (Functions, Injections, Restriction, Surjections,
+                        Bijections, Image, InvImage)
 
 def is_infinite_set(expr):
     if hasattr(expr, 'is_infinite_set'):
diff --git a/packages/proveit/logic/sets/functions/__init__.py b/packages/proveit/logic/sets/functions/__init__.py
index b6ceda0a2202..8ff4448a3652 100644
--- a/packages/proveit/logic/sets/functions/__init__.py
+++ b/packages/proveit/logic/sets/functions/__init__.py
@@ -1,4 +1,5 @@
 from .functions import Functions
+from .restriction import Restriction 
 from .images import Image, InvImage
 from .injections import Injections
 from .surjections import Surjections
diff --git a/packages/proveit/logic/sets/functions/_theory_nbs_/axioms.ipynb b/packages/proveit/logic/sets/functions/_theory_nbs_/axioms.ipynb
index 82089ebb803e..7b25c1c1f575 100644
--- a/packages/proveit/logic/sets/functions/_theory_nbs_/axioms.ipynb
+++ b/packages/proveit/logic/sets/functions/_theory_nbs_/axioms.ipynb
@@ -18,9 +18,10 @@
     "# 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 f, x, A, B, fx\n",
+    "from proveit import f, x, A, B, R, fx, Conditional, ConditionalSet, Function\n",
     "from proveit.logic import And, Equals, FALSE, Forall, InSet, NotInSet\n",
-    "from proveit.logic.sets import Functions"
+    "from proveit.logic.sets import Functions, Restriction, SubsetEq\n",
+    "from proveit.logic.sets.functions import undefined"
    ]
   },
   {
@@ -36,7 +37,7 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "A function from a domain $A$ to codomain $B$ must map any element in $A$ to an element in $B$."
+    "Specifying a function $f:A\\rightarrow B$ with domain $A$ and codomain $B$ means two things: (1) for all $x \\in A$ we have $f(x) \\in B$; and (2) if $x \\notin A$, then $f(x)$ is undefined (otherwise we should re-define the domain $A$)."
    ]
   },
   {
@@ -48,7 +49,34 @@
     "functions_def = Forall(\n",
     "    (f, A, B), Equals(InSet(f, Functions(A, B)),\n",
     "                      And(Forall(x, InSet(fx, B), domain=A),\n",
-    "    Forall(x, Equals(fx, FALSE), conditions = [NotInSet(x, A)]))))"
+    "    Forall(x, Equals(fx, undefined), conditions = [NotInSet(x, A)]))))"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "The restriction of a function $f:A \\rightarrow B$ to some new domain $R \\subseteq A$ creates a new function $f\\vert_{R}:R \\rightarrow B$ whose outputs agree with the original function on the restricted domain:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "restriction_def = (\n",
+    "    Forall((A, B, R),\n",
+    "    Forall(f,\n",
+    "    Forall(x,\n",
+    "           Equals(\n",
+    "           Function(Restriction(f, R), x),\n",
+    "           ConditionalSet(Conditional(fx, InSet(x, R)), Conditional(undefined, NotInSet(x, R)))\n",
+    "           )),\n",
+    "    domain = Functions(A, B)),\n",
+    "    conditions = [SubsetEq(R, A)]\n",
+    "    )\n",
+    ")"
    ]
   },
   {
diff --git a/packages/proveit/logic/sets/functions/_theory_nbs_/demonstrations.ipynb b/packages/proveit/logic/sets/functions/_theory_nbs_/demonstrations.ipynb
index a813f7cdbdf5..afa48194b5e9 100644
--- a/packages/proveit/logic/sets/functions/_theory_nbs_/demonstrations.ipynb
+++ b/packages/proveit/logic/sets/functions/_theory_nbs_/demonstrations.ipynb
@@ -15,15 +15,119 @@
    "outputs": [],
    "source": [
     "import proveit\n",
+    "from proveit import f, x, A, B, C, R, fx\n",
+    "from proveit.logic import Forall, Functions, InSet\n",
+    "from proveit.logic.sets import Restriction\n",
     "%begin demonstrations"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "#### $\\texttt{Functions}(A, B)$, the set of all functions $f:A \\rightarrow B$ with domain $A$ and codomain $B$"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InSet(f, Functions(A, B))"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InSet(f, Functions(A, B)).definition()"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InSet(f, Functions(A, B)).as_defined()"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InSet(f, Functions(A, B)).conclude(\n",
+    "        assumptions = [Forall(x, InSet(fx, B), domain = A)]\n",
+    ")"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InSet(f, Functions(A, B)).unfold(\n",
+    "        assumptions = [InSet(f, Functions(A, B))])"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "#### $f\\vert_{R}$, the restriction of $f:A \\rightarrow B$ to new domain $R \\subseteq A$."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "Restriction(f, R)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from proveit.logic.sets.functions import restriction_def\n",
+    "restriction_def"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,
    "metadata": {},
    "outputs": [],
-   "source": []
+   "source": [
+    "from proveit.logic import SubsetEq\n",
+    "restriction_def_inst = restriction_def.instantiate({A:A, B:B, R:R, f:f},\n",
+    "        assumptions = [SubsetEq(R, A), InSet(f, Functions(A, B))])"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "And notice the `known_memberships` dictionary, which might be useful in constructing some Restriction() methods:"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "InSet.known_memberships[f]"
+   ]
   },
   {
    "cell_type": "code",
diff --git a/packages/proveit/logic/sets/functions/_theory_nbs_/proofs/restriction_membership/thm_proof.ipynb b/packages/proveit/logic/sets/functions/_theory_nbs_/proofs/restriction_membership/thm_proof.ipynb
new file mode 100644
index 000000000000..f7233f262891
--- /dev/null
+++ b/packages/proveit/logic/sets/functions/_theory_nbs_/proofs/restriction_membership/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\">functions</a>.<a class=\"ProveItLink\" href=\"../../theorems.ipynb#restriction_membership\">restriction_membership</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 restriction_membership"
+   ]
+  },
+  {
+   "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/functions/_theory_nbs_/theorems.ipynb b/packages/proveit/logic/sets/functions/_theory_nbs_/theorems.ipynb
index f2e38fcd91bd..f6dee8dd4dd0 100644
--- a/packages/proveit/logic/sets/functions/_theory_nbs_/theorems.ipynb
+++ b/packages/proveit/logic/sets/functions/_theory_nbs_/theorems.ipynb
@@ -18,10 +18,11 @@
     "# 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 Lambda, Conditional\n",
-    "from proveit import f, x, A, B, fx\n",
-    "from proveit.logic import Forall, Equals, InSet\n",
-    "from proveit.logic.sets import Functions"
+    "from proveit import Lambda, Conditional, ConditionalSet, Function\n",
+    "from proveit import f, x, A, B, R, fx\n",
+    "from proveit.logic import Forall, Equals, InSet, NotInSet, SubsetEq\n",
+    "from proveit.logic.sets import Functions, Restriction\n",
+    "from proveit.logic.sets.functions import undefined"
    ]
   },
   {
@@ -67,6 +68,20 @@
     "                                   Functions(A, B))))"
    ]
   },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "restriction_membership = (\n",
+    "    Forall((A, B, R),\n",
+    "    Forall(f, InSet(Restriction(f, R), Functions(R, B)),\n",
+    "           domain = Functions(A, B)),\n",
+    "    conditions = [SubsetEq(R, A)])\n",
+    ")"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": null,
diff --git a/packages/proveit/logic/sets/functions/restriction.py b/packages/proveit/logic/sets/functions/restriction.py
new file mode 100644
index 000000000000..7544afc10ce8
--- /dev/null
+++ b/packages/proveit/logic/sets/functions/restriction.py
@@ -0,0 +1,37 @@
+from proveit import Function, Literal, Operation
+
+class Restriction(Function):
+    '''
+    Given a function f: A -> B, with domain A and co-domain B,
+    and subset S of A, Restriction(f, S) represents the restriction
+    of the function f to domain S --- that is, g = Restriction(f, S)
+    is a new function such that g(x) = f(x) for all x in S and is
+    undefined for x not in S.
+    Restriction(f, S) is an element of the set of Functions(S, B).
+    The axiomatic definition includes the constraint that S be a
+    subset of the original domain A.
+    '''
+
+    # The literal operator for the Restriction function
+    # (see further below for actual latex and string implementations).
+    _operator_ = Literal('Restriction', r'\textrm{Restriction}',
+                         theory=__file__)
+    
+    def __init__(self, f, domain, *, styles=None):
+        # Represent f|_{S}, the restriction of function f: A -> B to
+        # the restricted domain S (where S is a subset of A).
+        Operation.__init__(
+                self, Restriction._operator_, (f, domain), 
+                styles=styles)
+        self.fxn = f
+        self.domain = domain
+    
+    def latex(self, **kwargs):
+        fxn_str = self.fxn.latex(fence=True)
+        domain_str = self.domain.latex(fence=True)
+        return (fxn_str + r'\vert_{'+ domain_str + r'}')
+
+    def string(self, **kwargs):
+        fxn_str    = self.fxn.string(fence=True)
+        domain_str = self.domain.string(fence=True)
+        return (fxn_str + r'_{' + domain_str + r'}')

From 5e6e1a6652c16f2e596b1b35200b806e429f87bd Mon Sep 17 00:00:00 2001
From: Warren Craft <wdcraft@unm.edu>
Date: Mon, 14 Jul 2025 09:53:28 -0600
Subject: [PATCH 4/4] Add comment for future consideration

Add comment in Restriction() class description for future consideration, possibly changing Restriction(f, S) to Restriction(f, A, B, S) to include the original domain and co-domain of the function f (since neither may be easily accessible from the Restriction(f, S) construction itself).
---
 packages/proveit/logic/sets/functions/restriction.py | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/packages/proveit/logic/sets/functions/restriction.py b/packages/proveit/logic/sets/functions/restriction.py
index 7544afc10ce8..ac5d883f51a1 100644
--- a/packages/proveit/logic/sets/functions/restriction.py
+++ b/packages/proveit/logic/sets/functions/restriction.py
@@ -10,6 +10,9 @@ class Restriction(Function):
     Restriction(f, S) is an element of the set of Functions(S, B).
     The axiomatic definition includes the constraint that S be a
     subset of the original domain A.
+    Future work: consider (re-)defining Restriction(f, S) to be
+    Restriction(f, A, B, S) so as to explicitly include the original
+    domain and co-domain of the function f.
     '''
 
     # The literal operator for the Restriction function
