Expand notes on function categories.

notes/.obsidian/plugins/obsidian-to-anki-plugin/data.json

@@ -137,7 +137,11 @@
     "venn-diagram-symm-diff.png",
     "relation-ordering-example.png",
     "open-addressing.png",
-    "closed-addressing.png"
+    "closed-addressing.png",
+    "function-bijective.png",
+    "function-injective.png",
+    "function-surjective.png",
+    "function-general.png"
   ],
   "File Hashes": {
     "algorithms/index.md": "3ac071354e55242919cc574eb43de6f8",
@@ -176,7 +180,7 @@
     "_journal/2024-02-02.md": "a3b222daee8a50bce4cbac699efc7180",
     "_journal/2024-02-01.md": "3aa232387d2dc662384976fd116888eb",
     "_journal/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970",
-    "logic/equiv-trans.md": "fb7f2027b2b323374580fde8a1de579e",
+    "logic/equiv-trans.md": "c52d0907d35d7a3c2e4576f2bd411257",
     "_journal/2024-02-07.md": "8d81cd56a3b33883a7706d32e77b5889",
     "algorithms/loop-invariants.md": "cbefc346842c21a6cce5c5edce451eb2",
     "algorithms/loop-invariant.md": "3b390e720f3b2a98e611b49a0bb1f5a9",
@@ -377,7 +381,7 @@
     "_journal/2024-04-16.md": "0bf6e2f2a3afab73d528cee88c4c1a92",
     "_journal/2024-04/2024-04-15.md": "256253b0633d878ca58060162beb7587",
     "algebra/polynomials.md": "da56d2d6934acfa2c6b7b2c73c87b2c7",
-    "algebra/sequences/delta-constant.md": "70f45d7b8d5c3a147fabc279105c4983",
+    "algebra/sequences/delta-constant.md": "d9af958375cdf993e4ac3c68c1324ba7",
     "_journal/2024-04-19.md": "a293087860a7f378507a96df0b09dd2b",
     "_journal/2024-04/2024-04-18.md": "f6e5bee68dbef90a21ca92a846930a88",
     "_journal/2024-04/2024-04-17.md": "331423470ea83fc990c1ee1d5bd3b3f1",
@@ -503,12 +507,12 @@
     "_journal/2024-06/2024-06-04.md": "52b28035b9c91c9b14cef1154c1a0fa1",
     "_journal/2024-06-06.md": "3f9109925dea304e7172df39922cc95a",
     "_journal/2024-06/2024-06-05.md": "b06a0fa567bd81e3b593f7e1838f9de1",
-    "set/relations.md": "303f83287d33a300cf8c7fafe2834235",
+    "set/relations.md": "d486836acec494ea3b185ec9746df7c9",
     "_journal/2024-06-07.md": "795be41cc3c9c0f27361696d237604a2",
     "_journal/2024-06/2024-06-06.md": "db3407dcc86fa759b061246ec9fbd381",
     "_journal/2024-06-08.md": "b20d39dab30b4e12559a831ab8d2f9b8",
     "_journal/2024-06/2024-06-07.md": "c6bfc4c1e5913d23ea7828a23340e7d3",
-    "lambda-calculus/alpha-conversion.md": "c0d40271a14b1f44b937de7791ca089b",
+    "lambda-calculus/alpha-conversion.md": "9965a24624a745af16f10d9ffd78cc0c",
     "lambda-calculus/index.md": "756c93b8717fd00b04f8a99509066486",
     "x86-64/instructions/condition-codes.md": "56ad6eb395153609a1ec51835925e8c9",
     "x86-64/instructions/logical.md": "818428b9ef84753920dc61e5c2de9199",
@@ -526,7 +530,12 @@
     "hashing/open-addressing.md": "c27e92f2865bbb426fdd1e30fc52f1ed",
     "hashing/closed-addressing.md": "962a48517969bf5e410cf78fc584051f",
     "_journal/2024-06-13.md": "dec86b3a3e43eca306c3cf9a46b260ed",
-    "_journal/2024-06/2024-06-12.md": "f82dfa74d0def8c3179d3d076f94558e"
+    "_journal/2024-06/2024-06-12.md": "f82dfa74d0def8c3179d3d076f94558e",
+    "_journal/2024-06-14.md": "5d12bc272238ac985a1d35d3d63ea307",
+    "_journal/2024-06/2024-06-13.md": "e2722a00585d94794a089e8035e05728",
+    "set/functions.md": "34bf35a8ae16a0d735ce7e3e1b5bfa05",
+    "_journal/2024-06-15.md": "92cb8dc5c98e10832fb70c0e3ab3cec4",
+    "_journal/2024-06/2024-06-14.md": "5d12bc272238ac985a1d35d3d63ea307"
   },
   "fields_dict": {
     "Basic": [

notes/_journal/2024-06-15.md

@@ -0,0 +1,11 @@
+---
+title: "2024-06-15"
+---
+
+- [x] Anki Flashcards
+- [x] KoL
+- [x] OGS
+- [ ] Sheet Music (10 min.)
+- [ ] Korean (Read 1 Story)
+
+* [[functions|Notes]] on injections, surjections, and bijections.

notes/_journal/2024-06/2024-06-14.md

@@ -0,0 +1,12 @@
+---
+title: "2024-06-14"
+---
+
+- [x] Anki Flashcards
+- [x] KoL
+- [x] OGS
+- [ ] Sheet Music (10 min.)
+- [ ] Korean (Read 1 Story)
+
+* Finished most notes on [[alpha-conversion|α-conversion]].
+* Starting notes on [[functions]].

notes/algebra/sequences/delta-constant.md

@@ -119,7 +119,7 @@ END%%
 
 %%ANKI
 Cloze
-The closed formula for a sequence will be a {degree $k$ polynomial} if and only if the $k$th differences {is constant}.
+The closed formula for a sequence will be a {degree $k$ polynomial} if and only if the $k$th differences are {constant}.
 Reference: Oscar Levin, *Discrete Mathematics: An Open Introduction*, 3rd ed., n.d., [https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf](https://discrete.openmathbooks.org/pdfs/dmoi3-tablet.pdf).
 <!--ID: 1713580109237-->
 END%%

notes/lambda-calculus/alpha-conversion.md

@@ -152,6 +152,8 @@ Let $x$, $y$, and $v$ be distinct variables. Then
 * $v \not\in FV(M) \Rightarrow [P/v][v/x]M \equiv_\alpha [P/x]M$
 * $v \not\in FV(M) \Rightarrow [x/v][v/x]M \equiv_\alpha M$
 * $y \not\in FV(P) \Rightarrow [P/x][Q/y]M \equiv_\alpha [([P/x]Q)/y][P/x]M$
+* $x \not\in FV(Q) \land y \not\in FV(P) \Rightarrow [P/x][Q/y]M \equiv_\alpha [Q/y][P/x]M$
+* $[P/x][Q/x]M \equiv_\alpha [([P/x]Q)/x]M$
 
 %%ANKI
 Basic
@@ -186,9 +188,8 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi
 END%%
 
 %%ANKI
-Basic
+Cloze
-$[P/v][v/x]M \equiv_\alpha [P/x]M$ is necessary for what condition?
+{$v \not\in FV(M)$} $\Rightarrow [P/v][v/x]M \equiv_\alpha [P/x]M$
-Back: $v \not\in FV(M)$
 Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
 <!--ID: 1717855810777-->
 END%%
@@ -266,16 +267,53 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi
 END%%
 
 %%ANKI
-Basic
+Cloze
-$[P/x][Q/y]M \equiv_\alpha [([P/x]Q)/y][P/x]M$ is necessary for what condition?
+{$y \not\in FV(P)$} $\Rightarrow [P/x][Q/y]M \equiv_\alpha [([P/x]Q)/y][P/x]M$
-Back: $y \not\in FV(P)$
 Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
 <!--ID: 1717855810784-->
 END%%
 
+%%ANKI
+Cloze
+{$x \not\in FV(Q) \land y \not\in FV(P)$} $\Rightarrow [P/x][Q/y]M \equiv_\alpha [Q/y][P/x]M$
+Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
+<!--ID: 1718422235903-->
+END%%
+
 %%ANKI
 Basic
-What happens if the antecedent is false in $y \not\in FV(P) \Rightarrow [P/x][Q/y]M \equiv_\alpha [([P/x]Q)/y][P/x]M$?
+$[P/x][Q/y]M \equiv_\alpha [Q/y][P/x]M$ is a specialization of what more general congruence?
+Back: $[P/x][Q/y]M \equiv_\alpha [([P/x]Q)/y][P/x]M$
+Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
+<!--ID: 1718422235909-->
+END%%
+
+%%ANKI
+Cloze
+{$F$} $\Rightarrow [P/x][Q/x]M \equiv_\alpha [([P/x]Q)/x]M$
+Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
+<!--ID: 1718422235912-->
+END%%
+
+%%ANKI
+Basic
+What expression containing nested substitutions is congruent to $[P/x][Q/x]M$?
+Back: $[([P/x]Q)/x]M$
+Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
+<!--ID: 1718422235916-->
+END%%
+
+%%ANKI
+Basic
+What expression containing adjacent substitutions is congruent to $[([P/x]Q)/x]M$?
+Back: $[P/x][Q/x]M$
+Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
+<!--ID: 1718422279995-->
+END%%
+
+%%ANKI
+Basic
+What happens if the antecedent of the following lemma is false? $$y \not\in FV(P) \Rightarrow [P/x][Q/y]M \equiv_\alpha [([P/x]Q)/y][P/x]M$$
 Back: $y$ is subbed in $M$ on the LHS but subbed in both $P$ and $M$ on the RHS.
 Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
 <!--ID: 1717855810787-->
@@ -313,6 +351,39 @@ Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combi
 <!--ID: 1717855810802-->
 END%%
 
+For $\lambda$-terms $M$, $M'$, $N$, and $N'$, and variable $x$, $$M \equiv_\alpha M' \land N \equiv_\alpha N' \Rightarrow [N/x]M \equiv_\alpha [N'/x]M'$$
+
+%%ANKI
+Basic
+The proof of which implication shows "substitution is well-behaved w.r.t. $\alpha$-conversion"?
+Back: $M \equiv_\alpha M' \land N \equiv_\alpha N' \Rightarrow [N/x]M \equiv_\alpha [N'/x]M'$
+Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
+<!--ID: 1718422973129-->
+END%%
+
+%%ANKI
+Basic
+What does Hindley et al. mean by "substitution is well-behaved w.r.t. $\alpha$-conversion"?
+Back: $\alpha$-converting substitution inputs yields congruent outputs.
+Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
+<!--ID: 1718422973135-->
+END%%
+
+%%ANKI
+Cloze
+{$M \equiv_\alpha M' \land N \equiv_\alpha N'$} $\Rightarrow [N/x]M \equiv_\alpha [N'/x]M'$
+Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
+<!--ID: 1718422973141-->
+END%%
+
+%%ANKI
+Basic
+What does Hindley et al. say the following implication says about substitution? $$M \equiv_\alpha M' \land N \equiv_\alpha N' \Rightarrow [N/x]M \equiv_\alpha [N'/x]M'$$
+Back: It is well-defined with respect to $\alpha$-conversion.
+Reference: Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).
+<!--ID: 1718422981125-->
+END%%
+
 ## Bibliography
 
 * Hindley, J Roger, and Jonathan P Seldin. “Lambda-Calculus and Combinators, an Introduction,” n.d. [https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf](https://www.cin.ufpe.br/~djo/files/Lambda-Calculus%20and%20Combinators.pdf).

notes/logic/equiv-trans.md

@@ -506,7 +506,7 @@ END%%
 %%ANKI
 Basic
 If $x \neq e$, why might $E_e^x = E$ be an equivalence despite $x$ existing in $E$?
-Back: If the only occurrences of $x$ in $E$ are bound.
+Back: The only occurrences of $x$ in $E$ may be bound.
 Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
 <!--ID: 1707762304135-->
 END%%

notes/set/functions.md

@@ -0,0 +1,444 @@
+---
+title: Functions
+TARGET DECK: Obsidian::STEM
+FILE TAGS: set::function
+tags:
+  - function
+  - set
+---
+
+## Overview
+
+A **function** $F$ is a single-valued [[relations|relation]]. We say $F$ **maps $A$ into $B$**, denoted $F \colon A \rightarrow B$, if and only if $F$ is a function, $\mathop{\text{dom}}A$, and $\mathop{\text{ran}}F \subseteq B$.
+
+%%ANKI
+Basic
+Which of relations or functions is the more general concept?
+Back: Relations.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443345-->
+END%%
+
+%%ANKI
+Basic
+What *is* a function?
+Back: A relation $F$ such that for each $x \in \mathop{\text{dom}}F$, there exists a unique $y$ such that $xFy$.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443366-->
+END%%
+
+%%ANKI
+Basic
+For function $F$ and $x \in \mathop{\text{dom}}F$, what name is given to $F(x)$?
+Back: The value of $F$ at $x$.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443370-->
+END%%
+
+%%ANKI
+Basic
+Who introduced the function notation $F(x)$?
+Back: Leonhard Euler.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443374-->
+END%%
+
+%%ANKI
+Basic
+Let $F$ be a function and $\langle x, y \rangle \in F$. Rewrite the membership as an expression excluding $y$.
+Back: $\langle x, F(x) \rangle \in F$
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443379-->
+END%%
+
+%%ANKI
+Basic
+Let $F$ be a function and $\langle x, y \rangle \in F$. Rewrite the membership as an expression excluding $x$.
+Back: N/A.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443384-->
+END%%
+
+%%ANKI
+Basic
+Consider notation $F(x)$. What assumption is $F$ assumed to satisfy?
+Back: It is assumed to be a function.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443388-->
+END%%
+
+%%ANKI
+Basic
+Consider notation $F(x)$. What assumption is $x$ assumed to satisfy?
+Back: It is assumed to be in the domain of $F$.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443393-->
+END%%
+
+%%ANKI
+Cloze
+A function is a {single-valued} relation.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443397-->
+END%%
+
+%%ANKI
+Basic
+How is $F \colon A \rightarrow B$ pronounced?
+Back: $F$ maps $A$ into $B$.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443401-->
+END%%
+
+%%ANKI
+Basic
+What three conditions hold iff $F$ maps $A$ into $B$?
+Back: $F$ is a function, $\mathop{\text{dom}}F = A$, and $\mathop{\text{ran}}F \subseteq B$.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443404-->
+END%%
+
+%%ANKI
+Basic
+Consider function $F \colon A \rightarrow B$. What term is used to refer to $A$?
+Back: The domain.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718464126872-->
+END%%
+
+%%ANKI
+Basic
+Consider function $F \colon A \rightarrow B$. What term is used to refer to $B$?
+Back: The codomain.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718464126879-->
+END%%
+
+%%ANKI
+Basic
+How does the range of a function compare to its codomain?
+Back: The range is a subset of the codomain.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718464126883-->
+END%%
+
+## Injections
+
+A function is **injective** or **one-to-one** if each element of the codomain is mapped to by at most one element of the domain.
+
+%%ANKI
+Basic
+What does it mean for a function to be injective?
+Back: Each element of the codomain is mapped to by at most one element of the domain.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718464126887-->
+END%%
+
+%%ANKI
+Basic
+What does it mean for a function to be one-to-one?
+Back: Each element of the codomain is mapped to by at most one element of the domain.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718465870487-->
+END%%
+
+%%ANKI
+Basic
+Each element of an injection's codomain is mapped to by how many elements of the domain?
+Back: At most one.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718464498595-->
+END%%
+
+%%ANKI
+Basic
+Suppose `Function.Injective f` for $f \colon A \rightarrow B$. What predicate logical formula describes $f$?
+Back: $\forall a_1, a_2 \in A, (f(a_1) = f(a_2) \Rightarrow a_1 = a_2$)
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+Tags: lean logic::predicate
+<!--ID: 1718464498603-->
+END%%
+
+%%ANKI
+Basic
+Does the following depict an injection?
+![[function-bijective.png]]
+Back: Yes.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718465870490-->
+END%%
+
+%%ANKI
+Basic
+Does the following depict a one-to-one function?
+![[function-injective.png]]
+Back: Yes.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718465870493-->
+END%%
+
+%%ANKI
+Basic
+Does the following depict a one-to-one function?
+![[function-surjective.png]]
+Back: No.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718465870497-->
+END%%
+
+%%ANKI
+Basic
+*Why* isn't the following an injection?
+![[function-general.png]]
+Back: Both $1 \mapsto d$ and $2 \mapsto d$.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718465870505-->
+END%%
+
+%%ANKI
+Basic
+Is a single-valued set a function?
+Back: Not necessarily.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443358-->
+END%%
+
+%%ANKI
+Basic
+Is a single-valued relation a function?
+Back: Yes.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443362-->
+END%%
+
+%%ANKI
+Basic
+Is a single-rooted set a function?
+Back: Not necessarily.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718465870509-->
+END%%
+
+%%ANKI
+Basic
+Is a single-rooted relation a function?
+Back: Not necessarily.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718465870519-->
+END%%
+
+%%ANKI
+Cloze
+{One-to-one} is to functions whereas {single-rooted} is to relations.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718465870525-->
+END%%
+
+%%ANKI
+Basic
+Is a one-to-one function a single-rooted relation?
+Back: Yes.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718465870531-->
+END%%
+
+%%ANKI
+Basic
+Is a single-rooted relation a one-to-one function?
+Back: Not necessarily.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718465870536-->
+END%%
+
+%%ANKI
+Basic
+Is a single-rooted function a one-to-one function?
+Back: Yes.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718465870541-->
+END%%
+
+## Surjections
+
+A function is **surjective** or **onto** if each element of the codomain is mapped to by at least one element of the domain. That is, **$F$ maps $A$ onto $B$** if and only if $F$ is a function, $\mathop{\text{dom}}A$, and $\mathop{\text{ran}}F = B$.
+
+%%ANKI
+Basic
+What does it mean for function to be surjective?
+Back: Each element of the codomain is mapped to by at least one element of the domain.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718464126891-->
+END%%
+
+%%ANKI
+Basic
+What does it mean for a function to be onto?
+Back: Each element of the codomain is mapped to by at least one element of the domain.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718465870546-->
+END%%
+
+%%ANKI
+Basic
+Each element of a surjection's codomain is mapped to by how many elements of the domain?
+Back: At least one.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718464498606-->
+END%%
+
+%%ANKI
+Basic
+Suppose `Function.Surjective f` for $f \colon A \rightarrow B$. What predicate logical formula describes $f$?
+Back: $\forall b \in B, \exists a \in A, f(a) = b$
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+Tags: lean logic::predicate
+<!--ID: 1718464498615-->
+END%%
+
+%%ANKI
+Cloze
+{1:Injective} is to {2:one-to-one} as {2:surjective} is to {1:onto}.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718464126897-->
+END%%
+
+%%ANKI
+Basic
+What three conditions hold iff $F$ maps $A$ onto $B$?
+Back: $F$ is a function, $\mathop{\text{dom}}F = A$, and $\mathop{\text{ran}}F = B$.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443408-->
+END%%
+
+%%ANKI
+Basic
+Let $F$ map $A$ into $B$. Does $F$ map $A$ onto $B$?
+Back: Not necessarily.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443412-->
+END%%
+
+%%ANKI
+Basic
+Let $F$ map $A$ onto $B$. Does $F$ map $A$ into $B$?
+Back: Yes.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443415-->
+END%%
+
+%%ANKI
+Cloze
+Let $F$ be a function. Then $F$ maps {$\mathop{\text{dom}}F$} onto {$\mathop{\text{ran}}F$}.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443419-->
+END%%
+
+%%ANKI
+Basic
+Does the following depict a surjection?
+![[function-bijective.png]]
+Back: Yes.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718465870552-->
+END%%
+
+%%ANKI
+Basic
+Does the following depict an onto function?
+![[function-injective.png]]
+Back: No.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718465870558-->
+END%%
+
+%%ANKI
+Basic
+Does the following depict an onto function?
+![[function-surjective.png]]
+Back: Yes.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718465870565-->
+END%%
+
+%%ANKI
+Basic
+*Why* isn't the following a surjection?
+![[function-general.png]]
+Back: No element of $X$ maps to $b \in Y$.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718465870573-->
+END%%
+
+## Bijections
+
+A function is **bijective** or a **one-to-one correspondence** if each element of the codomain is mapped to by exactly one element of the domain.
+
+%%ANKI
+Basic
+What does it mean for a function to be bijective?
+Back: It is both injective and surjective.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718464728903-->
+END%%
+
+%%ANKI
+Basic
+Each element of a bijection's codomain is mapped to by how many elements of the domain?
+Back: Exactly one.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718464728907-->
+END%%
+
+%%ANKI
+Cloze
+{1:Injective} is to {2:one-to-one} as {2:bijective} is to {1:one-to-one correspondence}.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718464728899-->
+END%%
+
+%%ANKI
+Cloze
+{1:Surjective} is to {2:onto} as {2:bijective} is to {1:one-to-one correspondence}.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718465870579-->
+END%%
+
+%%ANKI
+Basic
+Does the following depict a bijection?
+![[function-bijective.png]]
+Back: Yes.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718465870585-->
+END%%
+
+%%ANKI
+Basic
+*Why* isn't the following a one-to-one correspondence?
+![[function-injective.png]]
+Back: The function does not map onto $Y$.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718465870592-->
+END%%
+
+%%ANKI
+Basic
+*Why* isn't the following a one-to-one correspondence?
+![[function-surjective.png]]
+Back: The function is not one-to-one.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718465870599-->
+END%%
+
+%%ANKI
+Basic
+What distinguishes a one-to-one function from a one-to-one correspondence?
+Back: The former is not necessarily surjective.
+Reference: “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+<!--ID: 1718465870605-->
+END%%
+
+## Bibliography
+
+* “Bijection, Injection and Surjection,” in _Wikipedia_, May 2, 2024, [https://en.wikipedia.org/w/index.php?title=Bijection_injection_and_surjection](https://en.wikipedia.org/w/index.php?title=Bijection,_injection_and_surjection&oldid=1221800163).
+* Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).

notes/set/relations.md

@@ -345,6 +345,24 @@ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Pre
 <!--ID: 1718327739961-->
 END%%
 
+A set $A$ is **single-valued** iff for each $x$ in $\mathop{\text{dom}}A$, there is only one $y$ such that $xAy$. A set $A$ is **single-rooted** iff for each $y \in \mathop{\text{ran}}A$, there is only one $x$ such that $xAy$.
+
+%%ANKI
+Basic
+What does it mean for a set $A$ to be "single-valued"?
+Back: For each $x \in \mathop{\text{dom}}A$, there exists a unique $y$ such that $xAy$.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443355-->
+END%%
+
+%%ANKI
+Basic
+What does it mean for a set $A$ to be "single-rooted"?
+Back: For each $y \in \mathop{\text{ran}}A$, there exists a unique $x$ such that $xRy$.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718465870483-->
+END%%
+
 ## n-ary Relations
 
 We define ordered triples as $\langle x, y, z \rangle = \langle \langle x, y \rangle, z \rangle$. We define ordered quadruples as $\langle x_1, x_2, x_3, x_4 \rangle = \langle \langle \langle x_1, x_2 \rangle, x_3 \rangle, x_4 \rangle$. This idea generalizes to $n$-tuples. As a special case, we define the $1$-tuple $\langle x \rangle = x$.
@@ -407,6 +425,14 @@ Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Pre
 <!--ID: 1718329620114-->
 END%%
 
+%%ANKI
+Basic
+What does it mean for a relation to be on some set $A$?
+Back: The components of the relation's members are members of $A$.
+Reference: Herbert B. Enderton, *Elements of Set Theory* (New York: Academic Press, 1977).
+<!--ID: 1718427443424-->
+END%%
+
 %%ANKI
 Basic
 A $2$-ary relation on $A$ is a subset of what Cartesian product?