Appendix.qmd

# Appendix {.unnumbered}
\markdouble{Appendix}

## Tactics Used

Tactics marked with an asterisk (*) are defined in the file `HTPIDefs.lean` in the HTPI Lean Package that accompanies this book.  They will not work without that file.  The others are standard Lean tactics or are defined in Lean's mathematics library, `mathlib`.

::: {style="margin: 0% 10%"}
| Tactic | Where Introduced |
|:--|:----|
| `apply` | [Sections 3.1 & 3.2](Chap3.html#proofs-involving-negations-and-conditionals) |
| `apply?` | [Section 3.6](Chap3.html#existence-and-uniqueness-proofs) |
| `assume`* | [Introduction to Lean: A First Example](IntroLean.html#a-first-example) |
| `bicond_neg`* | [Introduction to Lean: Tactic Mode](IntroLean.html#tactic-mode) |
| `by_cases` | [Section 3.5](Chap3.html#proofs-involving-disjunctions) |
| `by_cases on`* | [Section 3.5](Chap3.html#proofs-involving-disjunctions) |
| `by_contra` | [Sections 3.1 & 3.2](Chap3.html#proofs-involving-negations-and-conditionals) |
| `by_induc`* | [Section 6.1](Chap6.html#proof-by-mathematical-induction) |
| `by_strong_induc`* | [Section 6.4](Chap6.html#strong-induction) |
| `conditional`* | [Introduction to Lean: Tactic Mode](IntroLean.html#tactic-mode) |
| `contradict`* | [Sections 3.1 & 3.2](Chap3.html#proofs-involving-negations-and-conditionals) |
| `contrapos`* | [Introduction to Lean: A First Example](IntroLean.html#a-first-example) |
| `decide` | [Section 6.1](Chap6.html#proof-by-mathematical-induction) |
| `define`* | [Introduction to Lean: Types](IntroLean.html#types) |
| `demorgan`* | [Introduction to Lean: Tactic Mode](IntroLean.html#tactic-mode) |
| `disj_syll`* | [Section 3.5](Chap3.html#proofs-involving-disjunctions) |
| `double_neg`* | [Introduction to Lean: Tactic Mode](IntroLean.html#tactic-mode) |
| `exact` | [Section 3.6](Chap3.html#existence-and-uniqueness-proofs) |
| `exists_unique`* | [Section 3.6](Chap3.html#existence-and-uniqueness-proofs) |
| `fix`* | [Section 3.3](Chap3.html#proofs-involving-quantifiers) |
| `have` | [Introduction to Lean: A First Example](IntroLean.html#a-first-example) |
| `linarith` | [Section 6.1](Chap6.html#proof-by-mathematical-induction) |
| `obtain`* | [Section 3.3](Chap3.html#proofs-involving-quantifiers) |
| `or_left`* | [Section 3.5](Chap3.html#proofs-involving-disjunctions) |
| `or_right`* | [Section 3.5](Chap3.html#proofs-involving-disjunctions) |
| `push Not` | [Section 8.1](Chap8.html#equinumerous-sets) |
| `quant_neg`* | [Section 3.3](Chap3.html#proofs-involving-quantifiers) |
| `rel` | [Section 6.3](Chap6.html#recursion) |
| `rewrite` | [Section 3.6](Chap3.html#existence-and-uniqueness-proofs) |
| `rfl` | [Section 3.7](Chap3.html#more-examples-of-proofs) |
| `ring` | [Section 3.7](Chap3.html#more-examples-of-proofs) |
| `rw` | [Section 3.7](Chap3.html#more-examples-of-proofs) |
| `set` | [Section 4.5](Chap4.html#equivalence-relations) |
| `show`* | [Introduction to Lean: A First Example](IntroLean.html#a-first-example) |
| `trivial` | [Section 7.2](Chap7.html#prime-factorization) |
:::

## Summary of Proof Techniques in Lean

### To Prove a Goal of the Form ...

#### `¬P`

The tactic `by_contra h` will initiate a proof by contradiction by introducing the new given `h : P` and setting the goal to be `False`.  (See also the tactics for reexpressing negative statements under the [Reexpressing Statements](#reex) heading below.  There is also further information about [proof by contradiction](#contrad) below.)

#### `P → Q`

The tactic `assume h : P` will introduce the new given `h : P` and set the goal to be `Q`.  (See also the `contrapos` tactic under the [Reexpressing Statements](#reex) heading below.)

#### `P ∧ Q`

If you have `h1 : P` and `h2 : Q`, then `And.intro h1 h2` is a proof of `P ∧ Q`.  If you have `h : P`, then the tactic `apply And.intro h` will set the goal to be `Q`, and if you have `h : Q`, then `apply And.intro _ h` will set the goal to be `P`.  If you don't already have a proof of either `P` or `Q`, then `apply And.intro` will set `P` and `Q` as separate goals.

#### `P ∨ Q`

If you have `h : P`, then `Or.intro_left Q h` is a proof of `P ∨ Q`.  Usually there is no need to specify `Q`, and `Or.inl h` will be recognized as a proof of `P ∨ Q`.  Similarly, if you have `h : Q`, then `Or.intro_right P h` and `Or.inr h` are proofs of `P ∨ Q`.

If you don't already have a proof of either `P` or `Q`, then the tactic `apply Or.inl` will set the goal to be `P`, and `apply Or.inr` will set the goal to be `Q`.  Also, the tactic `or_left with h` will introduce the new given `h : ¬Q` and set the goal to be `P`, and `or_right with h` will introduce the new given `h : ¬P` and set the goal to be `Q`.

Proof by cases is sometimes useful for proving disjunctions.  There is further information about [proof by cases](#cases) below.

#### `P ↔ Q`

If you have `h1 : P → Q` and `h2 : Q → P`, then `Iff.intro h1 h2` is a proof of `P ↔ Q`.  If you have `h : P → Q`, then the tactic `apply Iff.intro h` will set the goal to be `Q → P`, and if you have `h : Q → P`, then `apply Iff.intro _ h` will set the goal to be `P → Q`.  If you don't already have a proof of either `P → Q` or `Q → P`, then `apply Iff.intro` will set `P → Q` and `Q → P` as separate goals.

If `P` and `Q` are definitionally equal, then the tactic `rfl` will prove `P ↔ Q`.

#### `∀ (x : U), P x`

The tactic `fix x : U` will introduce the new variable `x : U` and set the goal to be `P x`.

#### `∃ (x : U), P x`

If you have `a : U` and `h : P a`, then `Exists.intro a h` is a proof of `∃ (x : U), P x`.  If you have `a : U` but you don't have a proof of `P a`, then the tactic `apply Exists.intro a` will set the goal to be `P a`.

#### `∃! (x : U), P x`

The tactic `exists_unique` will set `∃ (x : U), P x` and `∀ (x_1 x_2 : U), P x_1 → P x_2 → x_1 = x_2` as separate goals.

#### `∀ (n : Nat), P n`

The tactic `by_induc` will set `P 0` and `∀ (n : Nat), P n → P (n + 1)` as separate goals.  (If the goal is `∀ n ≥ k, P n`, then the `by_induc` tactic will use `k` as the base case rather than `0`.)  The tactic `by_strong_induc` will set the goal to be `∀ (n : Nat), (∀ n_1 < n, P n_1) → P n`.

### To Use a Given of the Form ...

#### `h : ¬P`

If you also have `h1 : P`, then `h h1` is a proof of `False` and `absurd h1 h` will be recognized as a proof of any statement.  If your goal is `False`, then `contradict h` will set the goal to be `P`.  (See also the tactics for reexpressing negative statements under the [Reexpressing Statements](#reex) heading below.  There is also further information about [proof by contradiction](#contrad) below.)

#### `h : P → Q`

If you also have `h1 : P`, then `h h1` is a proof of `Q`.  (See also the `contrapos` tactic under the [Reexpressing Statements](#reex) heading below.)

#### `h : P ∧ Q`

`h.left` is a proof of `P`, and `h.right` is a proof of `Q`.

#### `h : P ∨ Q`

The tactic `by_cases on h` will initiate a proof by cases; in case 1, `h` will be changed to `h : P`, and in case 2 it will be changed to `h : Q`.  If you want to preserve the original `h`, then `by_cases on h with h1` will introduce new givens `h1 : P` in case 1 and `h1 : Q` in case 2; `by_cases on h with h1, h2` will will introduce new givens `h1 : P` in case 1 and `h2 : Q` in case 2.  (There is further information about [proof by cases](#cases) below.)

If you have `h1 : ¬P`, then `disj_syll h h1` will change `h` to `h : Q`; if you want to preserve the original `h`, then `disj_syll h h1 with h2` will introduce the new given `h2 : Q`.  Similarly, if you have `h1 : ¬Q`, then `disj_syll h h1` will change `h` to `h : P`, and `disj_syll h h1 with h2` will introduce the new given `h2 : P`.

#### `h : P ↔ Q`

`h.ltr` is a proof of `P → Q` and `h.rtl` is a proof of `Q → P`.  (See also the `rewrite` tactic under the [Reexpressing Statements](#reex) heading below.)

#### `h : ∀ (x : U), P x`

If you have `a : U`, then `h a` is a proof of `P a`.

#### `h : ∃ (x : U), P x`

The tactic `obtain (a : U) (h1 : P a) from h` will introduce both the new object `a : U` and the new given `h1 : P a`.

#### `h : ∃! (x : U), P x`

The tactic `obtain (a : U) (h1 : P a)` `(h2 : ∀ (x_1 x_2 : U), P x_1 → P x_2 → x_1 = x_2)` `from h` will introduce the new object `a : U` and new givens `h1 : P a` and `h2 : ∀ (x_1 x_2 : U), P x_1 → P x_2 → x_1 = x_2`.

### Other Techniques That Can Be Used in Any Proof

#### Proof by Contradiction {id="contrad"}

The tactic `by_contra h` will introduce a new given `h` that is the negation of the goal, and set the goal to be `False`.  Usually you will complete a proof by contradiction by proving contradictory statements `h1 : Q` and `h2 : ¬Q`.  Once you have proven such contradictory statements, either `h2 h1` or `absurd h1 h2` can be used as a proof of `False`.

If you are doing a proof by contradiction (so your goal is `False`) and you plan to complete the proof by contradicting some hypothesis `h1`, then the tactic `contradict h1` will set the goal to be the negation of `h1`.

The tactic `contradict h1 with h` is shorthand for `by_contra h; contradict h1`.

#### Proof by Cases {id="cases"}

If you have `h : P ∨ Q`, then the tactic `by_cases on h` will break your proof into two cases based on `h`.  In case 1, `h` will be changed to `h : P`, and in case 2, it will be changed to `h : Q`.  The tactic `by_cases on h with h1` will introduce new givens `h1 : P` in case 1 and `h1 : Q` in case 2.  The tactic `by cases on h with h1, h2` will introduce new givens `h1 : P` in case 1 and `h2 : Q` in case 2.

Another way to initiate a proof by cases is with the tactic `by_cases h : P`, which will introduce the new givens `h : P` in case 1 and `h : ¬P` in case 2.

### Working Backwards

If the expression `t _` would prove the goal if the blank were replaced with a proof of some statement `P`, then the tactic `apply t` will set the goal to be `P`.  More generally, if `t _ _ ... _` would prove the goal if the blanks were replaced with proofs of several statements, then `apply t` will set all of those statements to be separate goals.  The expression `t` can also contain blanks within it that will generate additional goals.  For example, if the goal is `P ∧ Q` and you have `h : Q`, then `apply And.intro _ h` will set the goal to be `P`.

### Making Assertions

If `t` is a term-mode proof of a statement `P`, then the tactic `have h : P := t` will introduce the new given `h : P`.  If you want to give a tactic-mode proof to justify `h`, then you can write `have h : P := by` and then write a tactic-mode proof of `P`.  The tactic-mode proof should be indented to set it off from the surrounding proof.

If `t` is a term-mode proof of a statement `P` and `P` is the goal, then the tactic `show P from t` will complete the proof.  The tactic `exact t` will also complete the proof.

### Reexpressing Statements {id="reex"}

All of the tactics in this section apply by default to the goal; they can be applied to a given `h` by adding `at h`.

If `t` is a proof of `a = b`, then the tactic `rewrite [t]` will replace `a` anywhere it appears with `b`, and `rewrite [←t]` will replace `b` with `a`.  Similarly, if `t` is a proof of `P ↔ Q`, then `rewrite [t]` will replace `P` with `Q` and `rewrite [←t]` will replace `Q` with `P`.  If `t` contains blanks, Lean will try to fill them in to produce a proof that can be used as a rewriting rule; as with the `apply` tactic, blanks at the end of a proof can be left out.  You can put a list of rewriting rules in the brackets (for example, `rewrite [t1, ←t2, t3]`), and the replacements will be performed one after another.

The tactic `rw` is the same as `rewrite`, except that after doing the rewriting, it tries to prove the goal by using the `rfl` tactic (see [Easy Proofs](#easy) below).

The tactic `define` will write out the definition of a statement.  If you want to define just a subexpression of the statement, then you can write `define : [subexpression]`.  For example, if the goal is `x ∈ A ∩ B → x ∈ C`, then `define : x ∈ A ∩ B` will change the goal to `x ∈ A ∧ x ∈ B → x ∈ C`.

The tactics `contrapos`, `demorgan`, `conditional`, `double_neg`, `bicond_neg`, and `quant_neg` rewrite statements by applying various logical laws; for details, see the tables about laws of [sentential](IntroLean.html#prop-tacs) and [quantificational](Chap3.html#quantneg-tac) logic.  As with the `define` tactic, you can add `: [subexpression]` to apply the law to the subexpression.  For example, if the goal is `P ∧ (Q → ¬R)`, then the tactic `contrapos : Q → ¬R` will change it to `P ∧ (R → ¬Q)`.

If the goal is a negative statement, then the tactic `push Not` will apply multiple laws about negations to "push" the negation as far as possible into the statement.

If `e` is an expression of type `U`, and you want to give it the name `n` in your proof, then the tactic `set n : U := e` will introduce the variable `n` to stand for `e`.

### Easy Proofs {id="easy"}

The tactic `rfl` proves statements of the form `a = a'` or `a ↔ a'`, if `a` and `a'` are definitionally equal.

The tactic `decide` proves statements that can be verified to be true by means of a calculation.

The tactic `trivial` proves some "obviously" true statements.

There is some overlap among these tactics; for example, all three could be used to prove `2 + 2 = 4`.

### Algebra

The tactic `ring` will try to prove a goal that is an equation by combining algebraic laws involving addition, subtraction, multiplication, and exponentiation with natural number exponents.

The tactic `linarith` will try to combine givens that are linear equations or inequalities to prove a goal that is a linear equation or equality, or to prove the goal `False` if the givens contradict each other.

If `t` is a proof of a statement asserting a relationship between two quantities, then the tactic `rel [t]` will try to prove a goal that can be obtained from that relationship by applying the same operation to both sides. The tactic will try to find a theorem in Lean’s library that says that the operation preserves the relationship, and if the theorem requires auxiliary positivity facts, it will try to prove those facts as well.

### Calculational Proofs

If `P`, `Q`, `R`, and `S` are statements, then you can prove `P ↔ S` by proving `P ↔ Q`, `Q ↔ R`, and `R ↔ S`.  Such proofs can conveniently be written as calculational proofs.  We often use calculational proofs with the `have` and `show` tactics.  For example, we might write:
```lean
  have h : P ↔ S :=
    calc P
      _ ↔ Q := [proof of P ↔ Q]
      _ ↔ R := [proof of Q ↔ R]
      _ ↔ S := [proof of R ↔ S]
```
The proofs of the individual lines can be either term-mode proofs or tactic-mode proofs (introduced with `by`).  Calculational proofs can also be used to string together equations or inequalities to prove an equation or inequality.

## Transitioning to Standard Lean

If you want to continue to use Lean to write mathematical proofs, you may want to learn more about Lean.  A good place to start is the [Lean Community website](https://leanprover-community.github.io/index.html).  The resources there use "standard" Lean, which is somewhat different from the Lean in this book.

In a few cases we have used notation in this book that differs from standard Lean notation.  For example, if `h` is a proof of `P ↔ Q`, then we have used `h.ltr` and `h.rtl` to denote proofs of the left-to-right and right-to-left directions of the biconditional.  The standard Lean notation for these is `h.mp` and `h.mpr`, respectively ("mp" and "mpr" stand for "modus ponens" and "modus ponens reverse").  As explained at the end of [Section 5.4](Chap5.html#closures), the notations `Pred U` and `Rel A B` denote the types `U → Prop` and `A → B → Prop`, respectively.  Although `Rel` is standard notation (defined in Lean's math library `mathlib`), `Pred` is not; the notation `BinRel A` is also not standard Lean.  In place of `Pred U` you should use `U → Prop`, and in place of `BinRel A` you should use `Rel A A`.

However, the biggest difference between the Lean in this book and standard Lean is that the tactics marked with an asterisk in the table above are not a part of standard Lean.  If you want to learn to write proofs in standard Lean, you'll need to learn replacements for those tactics.  We discuss some such replacements below.  Some of these replacements are built into Lean, and some are defined in `mathlib`.

* [`assume`, `fix`]{.lrg}

If you are proving `P → Q` and you want to begin by assuming `h : P`, in standard Lean you would begin your proof by writing `intro h`.  You don't need to specify that `h` is an identifier for the assumption `P`; Lean will figure that out on its own.

If you are proving `∀ (x : U), P x` and you want to begin by introducing the variable `x` to stand for an arbitrary object of type `U`, in standard Lean you would begin your proof by writing `intro x`.  Again, you don't need to specify the type of `x`, because Lean will figure it out.

Thus, the tactic `intro` does the job of both `assume` and `fix`.  Furthermore, you can introduce multiple assumptions or objects with a single use of the `intro` tactic: `intro a b c` is equivalent to `intro a; intro b; intro c`.

* [`bicond_neg`, `demorgan`, `double_neg`, `quant_neg`]{.lrg}

We have mostly used these tactics to reexpress negative statements as more useful positive statements.  The tactic `push Not` can be used for this purpose.

* [`by_cases on`]{.lrg}

If you have `h : P ∨ Q`, then you can break your proof into cases by using the tactic `rcases h with hP | hQ`.  In case 1, `h : P ∨ Q` will be replaced by `hP : P`, and in case 2 it will be replaced by `hQ : Q`.  In both cases, you have to prove the original goal.

Note that `by_cases h : P` is standard Lean; it is only the use of `on` after `by_cases` that is nonstandard.

* [`by_induc`, `by_strong_induc`]{.lrg}

We saw in Section 7.2 that if you are proving a statement of the form `∀ (l : List U), ...`, then you can begin a proof by induction on the length of `l` by using the tactic `apply List.rec`.  Similarly, if you are proving `∀ (n : Nat), ...`, you can begin a proof by induction by using the tactic `apply Nat.recAux`.  For strong induction, you can use `apply Nat.strongRec`.

There is also a tactic `induction` that you may want to learn about.

* [`conditional`]{.lrg}

The commands `#check @imp_iff_not_or` and `#check @not_imp` produce the results

::: {.ind}
```
@imp_iff_not_or : ∀ {a b : Prop}, a → b ↔ ¬a ∨ b
@not_imp : ∀ {a b : Prop}, ¬(a → b) ↔ a ∧ ¬b
```
:::

Thus, `rewrite [imp_iff_not_or]` will convert a statement of the form `P → Q` into `¬P ∨ Q`, and `rewrite [←imp_iff_not_or]` will go in the other direction.  Similarly, `rewrite [not_imp]` will convert a statement of the form `¬(P → Q)` into `P ∧ ¬Q`, and `rewrite [←not_imp]` will go in the other direction.

* [`contradict`]{.lrg}

Suppose your goal is `False` (as it would be if you are doing a proof by contradiction), and you have `h : ¬P`.  Recall that Lean treats `¬P` as meaning the same thing as `P → False`, and therefore `h _` will prove the goal, if the blank is filled in with a proof of `P`.  It follows that `apply h` will set `P` as the goal.  In other words, in this situation `apply h` has the same effect as `contradict h`.

You could also get the same effect with the tactic `suffices hP : P from h hP`.  Think of this as meaning "it would suffice now to prove `P`, because if `hP` were a proof of `P`, then `h hP` would prove the goal."  Lean therefore sets `P` to be the goal.

Similarly, in a proof by contradiction, if you have `h : P`, then `suffices hnP : ¬P from hnP h` will set `¬P` as the goal.

Yet another possibility is `contrapose! h`.  (This is a variant on the `contrapose!` tactic, discussed in the next section.)

* [`contrapos`]{.lrg}

If your goal is a conditional statement, then the tactics `contrapose` and `contrapose!` will replace the goal with its contrapositive (`contrapose!` also uses `push Not` to try to simplify the negated statements that arise when forming a contrapositive).  You may also find the theorem `not_imp_not` useful:

::: {.ind}
```
@not_imp_not : ∀ {a b : Prop}, ¬a → ¬b ↔ b → a
```
:::

* [`define`]{.lrg}

The tactic `whnf` (which stands for "weak head normal form") is similar to `define`, although it sometimes produces results that
are a little confusing.

Another way to write out definitions is to prove a lemma stating the definition and then use that lemma as a rewriting rule in the `rewrite` tactic.  See, for example, the use of the theorem `inv_def` in [Section 4.2](Chap4.html#relations).

* [`disj_syll`]{.lrg}

The following theorems can be useful:

::: {.ind id="resolves"}
```
@Or.resolve_left : ∀ {a b : Prop}, a ∨ b → ¬a → b
@Or.resolve_right : ∀ {a b : Prop}, a ∨ b → ¬b → a
@Or.neg_resolve_left : ∀ {a b : Prop}, ¬a ∨ b → a → b
@Or.neg_resolve_right : ∀ {a b : Prop}, a ∨ ¬b → b → a
```
:::

For example, if you have `h1 : P ∨ Q` and `h2 : ¬P`, then `Or.resolve_left h1 h2` is a proof of `Q`.

* [`exists_unique`]{.lrg}

If your goal is `∃! (x : U), P x` and you think that `a` is the unique value of `x` that makes `P x` true, then you can use the tactic `apply ExistsUnique.intro a`.  This will leave you with two goals to prove, `P a` and `∀ (y : U), P y → y = a`.

* [`obtain`]{.lrg}

If you have `h : ∃ (x : U), P x`, then the tactic `obtain ⟨u, h1⟩ := h` will introduce both `u : U` and `h1 : P u` into the tactic state.  Note that `u` and `h1` must be enclosed in angle brackets, `⟨ ⟩`.  To enter those brackets, type `\<` and `\>`.

If you have `h : ∃! (x : U), P x`, then `obtain ⟨u, h1, h2⟩ := h` will also introduce `u : U` and `h1 : P u` into the tactic state.  In addition, it will introduce `h2` as an identifier for a statement that is equivalent to `∀ (y : U), P y → y = u`.  (Unfortunately, the statement introduced is more complicated.)

You may also find the theorems `ExistsUnique.exists` and `ExistsUnique.unique` useful:

::: {.ind}
```
@ExistsUnique.exists : ∀ {α : Sort u_1} {p : α → Prop},
              (∃! (x : α), p x) → ∃ (x : α), p x
@ExistsUnique.unique : ∀ {α : Sort u_1} {p : α → Prop},
              (∃! (x : α), p x) → ∀ {y₁ y₂ : α}, p y₁ → p y₂ → y₁ = y₂
```
:::

* [`or_left`, `or_right`]{.lrg}

If your goal is `P ∨ Q`, then the tactics `or_left` and `or_right` let you assume that one of `P` and `Q` is false and prove the other.  One way to do that in standard Lean is to use proof by cases.  For example, to assume `P` is false and prove `Q` you might proceed as follows:

```lean
  -- Goal is P ∨ Q
  by_cases hP : P
  · -- Case 1. hP : P
    exact Or.inl hP
    done
  · -- Case 2. hP : ¬P
    apply Or.inr
    --We now have hP : ¬P, and goal is Q
    **done::
```
Another possibility is to use one of the [theorems](#resolves) `Or.resolve_left`, `Or.resolve_right`, `Or.neg_resolve_left`, or `Or.neg_resolve_right` (described under `disj_syll` above) to convert the goal to an implication.

* [`show`]{.lrg}

There is a `show` tactic in standard Lean, but it works a little differently from the `show` tactic we have used in this book.  When our goal was a statement `P` and we had an expression `t` that was a proof of `P`, we usually completed the proof by writing `show P from t`.  In standard Lean you can complete the proof by writing `exact t`, as explained near the end of [Section 3.6](Chap3.html#existence-and-uniqueness-proofs).

## Typing Symbols

::: {style="margin: 0% 10%"}
| Symbol | How To Type It |
|:--:|:----:|
| `¬` | `\not` or `\n` |
| `∧` | `\and` |
| `∨` | `\or` or `\v` |
| `→` | `\to` or `\r` or `\imp` |
| `↔` | `\iff` or `\lr` |
| `∀` | `\forall` or `\all` |
| `∃` | `\exists` or `\ex` |
| `⦃` | `\{{` |
| `⦄` | `\}}` |
| `=` | `=` |
| `≠` | `\ne` |
| `∈` | `\in` |
| `∉` | `\notin` or `\inn` |
| `⊆` | `\sub` |
| `⊈` | `\subn` |
| `∪` | `\union` or `\cup` |
| `∩` | `\inter` or `\cap` |
| `⋃₀` | `\U0` |
| `⋂₀` | `\I0` |
| `\` | `\\` |
| `∆` | `\symmdiff` |
| `∅` | `\emptyset` |
| `𝒫` | `\powerset` |
| `·` | `\.` |
| `←` | `\leftarrow` or `\l` |
| `↑` | `\uparrow` or `\u` |
| `ℕ` | `\N` |
| `ℤ` | `\Z` |
| `ℚ` | `\Q` |
| `ℝ` | `\R` |
| `ℂ` | `\C` |
| `≤` | `\le` |
| `≥` | `\ge` |
| `∣` | `\|` |
| `×` | `\times` or `\x` |
| `∘` | `\comp` or `\circ` |
| `≡` | `\==` |
| `∼` | `\sim` or `\~` |
| `ₛ` | `\_s` |
| `⟨` | `\<` |
| `⟩` | `\>` |
:::