Simplify lean link formatting.
parent
e8aa984b98
commit
d89200fd9d
File diff suppressed because it is too large
Load Diff
|
|
@ -18,41 +18,42 @@
|
|||
\section{\defined{Construction Sequence}}%
|
||||
\hyperlabel{ref:construction-sequence}
|
||||
|
||||
A \textbf{construction sequence} is a finite sequence
|
||||
$\langle \epsilon_1, \ldots, \epsilon_n \rangle$ of expressions such that for
|
||||
each $i \leq n$ we have at least one of
|
||||
\begin{align*}
|
||||
& \epsilon_i \text{ is a sentence symbol} \\
|
||||
& \epsilon_i = \mathcal{E}_\neg(\epsilon_j) \text{ for some } j < i \\
|
||||
& \epsilon_i = \mathcal{E}_\square(\epsilon_j, \epsilon_k)
|
||||
\text{ for some } j < i, k < i
|
||||
\end{align*}
|
||||
where $\square$ is one of the binary connectives $\land$, $\lor$,
|
||||
$\Rightarrow$, $\Leftrightarrow$.
|
||||
A \textbf{construction sequence} is a finite sequence
|
||||
$\langle \epsilon_1, \ldots, \epsilon_n \rangle$ of expressions such that
|
||||
for each $i \leq n$ we have at least one of
|
||||
\begin{align*}
|
||||
& \epsilon_i \text{ is a sentence symbol} \\
|
||||
& \epsilon_i = \mathcal{E}_\neg(\epsilon_j) \text{ for some } j < i \\
|
||||
& \epsilon_i = \mathcal{E}_\square(\epsilon_j, \epsilon_k)
|
||||
\text{ for some } j < i, k < i
|
||||
\end{align*}
|
||||
where $\square$ is one of the binary connectives $\land$, $\lor$,
|
||||
$\Rightarrow$, $\Leftrightarrow$.
|
||||
|
||||
\section{\defined{Expression}}%
|
||||
\hyperlabel{ref:expression}
|
||||
|
||||
An \textbf{expression} is a finite sequence of symbols.
|
||||
An \textbf{expression} is a finite sequence of symbols.
|
||||
|
||||
\section{\defined{Well-Formed Formula}}%
|
||||
\hyperlabel{ref:well-formed-formula}
|
||||
|
||||
An \nameref{ref:expression} that can be built up from the sentence symbols by
|
||||
applying some finite number of times the \textbf{formula-building operations}
|
||||
(on expressions) defined by the equations:
|
||||
\begin{align*}
|
||||
\mathcal{E}_{\neg}(\alpha)
|
||||
& = (\neg \alpha) \\
|
||||
\mathcal{E}_{\land}(\alpha, \beta)
|
||||
& = (\alpha \land \beta) \\
|
||||
\mathcal{E}_{\lor}(\alpha, \beta)
|
||||
& = (\alpha \lor \beta) \\
|
||||
\mathcal{E}_{\Rightarrow}(\alpha, \beta)
|
||||
& = (\alpha \Rightarrow \beta) \\
|
||||
\mathcal{E}_{\Leftrightarrow}(\alpha, \beta)
|
||||
& = (\alpha \Leftrightarrow \beta)
|
||||
\end{align*}
|
||||
An \nameref{ref:expression} that can be built up from the sentence symbols by
|
||||
applying some finite number of times the
|
||||
\textbf{formula-building operations} (on expressions) defined by the
|
||||
equations:
|
||||
\begin{align*}
|
||||
\mathcal{E}_{\neg}(\alpha)
|
||||
& = (\neg \alpha) \\
|
||||
\mathcal{E}_{\land}(\alpha, \beta)
|
||||
& = (\alpha \land \beta) \\
|
||||
\mathcal{E}_{\lor}(\alpha, \beta)
|
||||
& = (\alpha \lor \beta) \\
|
||||
\mathcal{E}_{\Rightarrow}(\alpha, \beta)
|
||||
& = (\alpha \Rightarrow \beta) \\
|
||||
\mathcal{E}_{\Leftrightarrow}(\alpha, \beta)
|
||||
& = (\alpha \Leftrightarrow \beta)
|
||||
\end{align*}
|
||||
|
||||
\endgroup
|
||||
|
||||
|
|
@ -65,19 +66,15 @@ An \nameref{ref:expression} that can be built up from the sentence symbols by
|
|||
\section{\sorry{Lemma 0A}}%
|
||||
\hyperlabel{sec:lemma-0a}
|
||||
|
||||
\begin{lemma}[0A]
|
||||
\begin{lemma}[0A]
|
||||
Assume that $\langle x_1, \ldots, x_m \rangle =
|
||||
\langle y_1, \ldots, y_m, \ldots, y_{m+k} \rangle$.
|
||||
Then $x_1 = \langle y_1, \ldots, y_{k+1} \rangle$.
|
||||
\end{lemma}
|
||||
|
||||
Assume that $\langle x_1, \ldots, x_m \rangle =
|
||||
\langle y_1, \ldots, y_m, \ldots, y_{m+k} \rangle$.
|
||||
Then $x_1 = \langle y_1, \ldots, y_{k+1} \rangle$.
|
||||
|
||||
\end{lemma}
|
||||
|
||||
\begin{proof}
|
||||
|
||||
TODO
|
||||
|
||||
\end{proof}
|
||||
\begin{proof}
|
||||
TODO
|
||||
\end{proof}
|
||||
|
||||
\chapter{Sentential Logic}%
|
||||
\hyperlabel{chap:sentential-logic}
|
||||
|
|
@ -88,18 +85,15 @@ Then $x_1 = \langle y_1, \ldots, y_{k+1} \rangle$.
|
|||
\subsection{\sorry{Induction Principle}}%
|
||||
\hyperlabel{sub:induction-principle-1}
|
||||
|
||||
\begin{theorem}
|
||||
\begin{theorem}
|
||||
If $S$ is a set of wffs containing all the sentence symbols and closed under
|
||||
all five formula-building operations, then $S$ is the set of \textit{all}
|
||||
wffs.
|
||||
\end{theorem}
|
||||
|
||||
If $S$ is a set of wffs containing all the sentence symbols and closed under all
|
||||
five formula-building operations, then $S$ is the set of \textit{all} wffs.
|
||||
|
||||
\end{theorem}
|
||||
|
||||
\begin{proof}
|
||||
|
||||
TODO
|
||||
|
||||
\end{proof}
|
||||
\begin{proof}
|
||||
TODO
|
||||
\end{proof}
|
||||
|
||||
\section{Exercises 1}%
|
||||
\hyperlabel{sec:exercises-1}
|
||||
|
|
@ -107,92 +101,81 @@ If $S$ is a set of wffs containing all the sentence symbols and closed under all
|
|||
\subsection{\sorry{Exercise 1.1.1}}%
|
||||
\hyperlabel{sub:exercise-1.1.1}
|
||||
|
||||
Give three sentences in English together with translations into our formal
|
||||
language.
|
||||
The sentences shoudl be chosen so as to have an interesting structure, and the
|
||||
translations should each contain 15 or more symbols.
|
||||
Give three sentences in English together with translations into our formal
|
||||
language.
|
||||
The sentences shoudl be chosen so as to have an interesting structure, and the
|
||||
translations should each contain 15 or more symbols.
|
||||
|
||||
\begin{answer}
|
||||
|
||||
TODO
|
||||
|
||||
\end{answer}
|
||||
\begin{answer}
|
||||
TODO
|
||||
\end{answer}
|
||||
|
||||
\subsection{\sorry{Exercise 1.1.2}}%
|
||||
\hyperlabel{sub:exercise-1.1.2}
|
||||
|
||||
Show that there are no wffs of length 2, 3, or 6, but that any other positive
|
||||
length is possible.
|
||||
Show that there are no wffs of length 2, 3, or 6, but that any other positive
|
||||
length is possible.
|
||||
|
||||
\begin{answer}
|
||||
|
||||
TODO
|
||||
|
||||
\end{answer}
|
||||
\begin{proof}
|
||||
TODO
|
||||
\end{proof}
|
||||
|
||||
\subsection{\sorry{Exercise 1.1.3}}%
|
||||
\hyperlabel{sub:exercise-1.1.3}
|
||||
|
||||
Let $\alpha$ be a wff; let $c$ be the number of places at which binary
|
||||
connective symbols $(\land, \lor, \Rightarrow, \Leftrightarrow)$ occur in
|
||||
$\alpha$; let $s$ be the number of places at which sentence symbols occur in
|
||||
$\alpha$.
|
||||
(For exmaple, if $\alpha$ is $(A \Rightarrow (\neg A))$ then $c = 1$ and $s = 2$.)
|
||||
Show by using the induction principle that $s = c + 1$.
|
||||
Let $\alpha$ be a wff; let $c$ be the number of places at which binary
|
||||
connective symbols $(\land, \lor, \Rightarrow, \Leftrightarrow)$ occur in
|
||||
$\alpha$; let $s$ be the number of places at which sentence symbols occur in
|
||||
$\alpha$.
|
||||
(For example, if $\alpha$ is $(A \Rightarrow (\neg A))$ then $c = 1$ and
|
||||
$s = 2$.)
|
||||
Show by using the induction principle that $s = c + 1$.
|
||||
|
||||
\begin{answer}
|
||||
|
||||
TODO
|
||||
|
||||
\end{answer}
|
||||
\begin{proof}
|
||||
TODO
|
||||
\end{proof}
|
||||
|
||||
\subsection{\sorry{Exercise 1.1.4}}%
|
||||
\hyperlabel{sub:exercise-1.1.4}
|
||||
|
||||
Assume we have a construction sequence ending in $\phi$, where $\phi$ does not
|
||||
contain the symbol $A_4$.
|
||||
Suppose we delete all the expressions in the construction sequence that contain
|
||||
$A_4$.
|
||||
Show that the result is still a legal construction sequence.
|
||||
Assume we have a construction sequence ending in $\phi$, where $\phi$ does not
|
||||
contain the symbol $A_4$.
|
||||
Suppose we delete all the expressions in the construction sequence that
|
||||
contain $A_4$.
|
||||
Show that the result is still a legal construction sequence.
|
||||
|
||||
\begin{answer}
|
||||
|
||||
TODO
|
||||
|
||||
\end{answer}
|
||||
\begin{proof}
|
||||
TODO
|
||||
\end{proof}
|
||||
|
||||
\subsection{\sorry{Exercise 1.1.5}}%
|
||||
\hyperlabel{sub:exercise-1.1.5}
|
||||
|
||||
Suppose that $\alpha$ is a wff not containing the negation symbol $\neg$.
|
||||
\begin{enumerate}[(a)]
|
||||
\item Show that the length of $\alpha$ (i.e., the number of symbols in the
|
||||
string) is odd.
|
||||
\item Show that more than a quarter of the symbols are sentence symbols.
|
||||
\end{enumerate}
|
||||
\textit{Suggestion}: Apply induction to show that the length is of the form
|
||||
$4k + 1$ and the number of sentence symbols is $k + 1$.
|
||||
Suppose that $\alpha$ is a wff not containing the negation symbol $\neg$.
|
||||
\begin{enumerate}[(a)]
|
||||
\item Show that the length of $\alpha$ (i.e., the number of symbols in the
|
||||
string) is odd.
|
||||
\item Show that more than a quarter of the symbols are sentence symbols.
|
||||
\end{enumerate}
|
||||
\textit{Suggestion}: Apply induction to show that the length is of the form
|
||||
$4k + 1$ and the number of sentence symbols is $k + 1$.
|
||||
|
||||
\begin{answer}
|
||||
|
||||
TODO
|
||||
|
||||
\end{answer}
|
||||
\begin{proof}
|
||||
TODO
|
||||
\end{proof}
|
||||
|
||||
\subsection{\sorry{Exercise 1.1.6}}%
|
||||
\hyperlabel{sub:exercise-1.1.6}
|
||||
|
||||
Suppose that $\alpha$ is a wff not containing the negation symbol $\neg$.
|
||||
\begin{enumerate}[(a)]
|
||||
\item Show that the length of $\alpha$ (i.e., the number of symbols in the
|
||||
string) is odd.
|
||||
\item Show that more than a quarter of the symbols are sentence symbols.
|
||||
\end{enumerate}
|
||||
Suppose that $\alpha$ is a wff not containing the negation symbol $\neg$.
|
||||
\begin{enumerate}[(a)]
|
||||
\item Show that the length of $\alpha$ (i.e., the number of symbols in the
|
||||
string) is odd.
|
||||
\item Show that more than a quarter of the symbols are sentence symbols.
|
||||
\end{enumerate}
|
||||
|
||||
\begin{answer}
|
||||
|
||||
TODO
|
||||
|
||||
\end{answer}
|
||||
\begin{proof}
|
||||
TODO
|
||||
\end{proof}
|
||||
|
||||
\end{document}
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -38,6 +38,153 @@ theorem commutative_law_ii (A B : Set α)
|
|||
exact and_comm
|
||||
_ = B ∩ A := rfl
|
||||
|
||||
/-! #### Associative Laws
|
||||
|
||||
For any sets `A`, `B`, and `C`,
|
||||
```
|
||||
A ∪ (B ∪ C) = (A ∪ B) ∪ C
|
||||
A ∩ (B ∩ C) = (A ∩ B) ∩ C
|
||||
```
|
||||
-/
|
||||
|
||||
#check Set.union_assoc
|
||||
|
||||
theorem associative_law_i (A B C : Set α)
|
||||
: A ∪ (B ∪ C) = (A ∪ B) ∪ C := calc A ∪ (B ∪ C)
|
||||
_ = { x | x ∈ A ∨ x ∈ B ∪ C } := rfl
|
||||
_ = { x | x ∈ A ∨ (x ∈ B ∨ x ∈ C) } := rfl
|
||||
_ = { x | (x ∈ A ∨ x ∈ B) ∨ x ∈ C } := by
|
||||
ext _
|
||||
simp only [Set.mem_setOf_eq]
|
||||
rw [← or_assoc]
|
||||
_ = { x | x ∈ A ∪ B ∨ x ∈ C } := rfl
|
||||
_ = (A ∪ B) ∪ C := rfl
|
||||
|
||||
#check Set.inter_assoc
|
||||
|
||||
theorem associative_law_ii (A B C : Set α)
|
||||
: A ∩ (B ∩ C) = (A ∩ B) ∩ C := calc A ∩ (B ∩ C)
|
||||
_ = { x | x ∈ A ∧ (x ∈ B ∩ C) } := rfl
|
||||
_ = { x | x ∈ A ∧ (x ∈ B ∧ x ∈ C) } := rfl
|
||||
_ = { x | (x ∈ A ∧ x ∈ B) ∧ x ∈ C } := by
|
||||
ext _
|
||||
simp only [Set.mem_setOf_eq]
|
||||
rw [← and_assoc]
|
||||
_ = { x | x ∈ A ∩ B ∧ x ∈ C } := rfl
|
||||
_ = (A ∩ B) ∩ C := rfl
|
||||
|
||||
/-! #### Distributive Laws
|
||||
|
||||
For any sets `A`, `B`, and `C`,
|
||||
```
|
||||
A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C)
|
||||
A ∪ (B ∩ C) = (A ∪ B) ∩ (A ∪ C)
|
||||
```
|
||||
-/
|
||||
|
||||
#check Set.inter_distrib_left
|
||||
|
||||
theorem distributive_law_i (A B C : Set α)
|
||||
: A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) := calc A ∩ (B ∪ C)
|
||||
_ = { x | x ∈ A ∧ x ∈ B ∪ C } := rfl
|
||||
_ = { x | x ∈ A ∧ (x ∈ B ∨ x ∈ C) } := rfl
|
||||
_ = { x | (x ∈ A ∧ x ∈ B) ∨ (x ∈ A ∧ x ∈ C) } := by
|
||||
ext _
|
||||
exact and_or_left
|
||||
_ = { x | x ∈ A ∩ B ∨ x ∈ A ∩ C } := rfl
|
||||
_ = (A ∩ B) ∪ (A ∩ C) := rfl
|
||||
|
||||
#check Set.union_distrib_left
|
||||
|
||||
theorem distributive_law_ii (A B C : Set α)
|
||||
: A ∪ (B ∩ C) = (A ∪ B) ∩ (A ∪ C) := calc A ∪ (B ∩ C)
|
||||
_ = { x | x ∈ A ∨ x ∈ B ∩ C } := rfl
|
||||
_ = { x | x ∈ A ∨ (x ∈ B ∧ x ∈ C) } := rfl
|
||||
_ = { x | (x ∈ A ∨ x ∈ B) ∧ (x ∈ A ∨ x ∈ C) } := by
|
||||
ext _
|
||||
exact or_and_left
|
||||
_ = { x | x ∈ A ∪ B ∧ x ∈ A ∪ C } := rfl
|
||||
_ = (A ∪ B) ∩ (A ∪ C) := rfl
|
||||
|
||||
/-! #### De Morgan's Laws
|
||||
|
||||
For any sets `A`, `B`, and `C`,
|
||||
```
|
||||
C - (A ∪ B) = (C - A) ∩ (C - B)
|
||||
C - (A ∩ B) = (C - A) ∪ (C - B)
|
||||
```
|
||||
-/
|
||||
|
||||
#check Set.diff_inter_diff
|
||||
|
||||
theorem de_morgans_law_i (A B C : Set α)
|
||||
: C \ (A ∪ B) = (C \ A) ∩ (C \ B) := calc C \ (A ∪ B)
|
||||
_ = { x | x ∈ C ∧ x ∉ A ∪ B } := rfl
|
||||
_ = { x | x ∈ C ∧ ¬(x ∈ A ∨ x ∈ B) } := rfl
|
||||
_ = { x | x ∈ C ∧ (x ∉ A ∧ x ∉ B) } := by
|
||||
ext _
|
||||
simp only [Set.mem_setOf_eq]
|
||||
rw [not_or_de_morgan]
|
||||
_ = { x | (x ∈ C ∧ x ∉ A) ∧ (x ∈ C ∧ x ∉ B) } := by
|
||||
ext _
|
||||
exact and_and_left
|
||||
_ = { x | x ∈ C \ A ∧ x ∈ C \ B } := rfl
|
||||
_ = (C \ A) ∩ (C \ B) := rfl
|
||||
|
||||
#check Set.diff_inter
|
||||
|
||||
theorem de_morgans_law_ii (A B C : Set α)
|
||||
: C \ (A ∩ B) = (C \ A) ∪ (C \ B) := calc C \ (A ∩ B)
|
||||
_ = { x | x ∈ C ∧ x ∉ A ∩ B } := rfl
|
||||
_ = { x | x ∈ C ∧ ¬(x ∈ A ∧ x ∈ B) } := rfl
|
||||
_ = { x | x ∈ C ∧ (x ∉ A ∨ x ∉ B) } := by
|
||||
ext _
|
||||
simp only [Set.mem_setOf_eq]
|
||||
rw [not_and_de_morgan]
|
||||
_ = { x | (x ∈ C ∧ x ∉ A) ∨ (x ∈ C ∧ x ∉ B) } := by
|
||||
ext _
|
||||
exact and_or_left
|
||||
_ = { x | x ∈ C \ A ∨ x ∈ C \ B } := rfl
|
||||
_ = (C \ A) ∪ (C \ B) := rfl
|
||||
|
||||
/-! #### Identities Involving ∅
|
||||
|
||||
For any set `A`,
|
||||
```
|
||||
A ∪ ∅ = A
|
||||
A ∩ ∅ = ∅
|
||||
A ∩ (C - A) = ∅
|
||||
```
|
||||
-/
|
||||
|
||||
#check Set.union_empty
|
||||
|
||||
theorem emptyset_identity_i (A : Set α)
|
||||
: A ∪ ∅ = A := calc A ∪ ∅
|
||||
_ = { x | x ∈ A ∨ x ∈ ∅ } := rfl
|
||||
_ = { x | x ∈ A ∨ False } := rfl
|
||||
_ = { x | x ∈ A } := by simp
|
||||
_ = A := rfl
|
||||
|
||||
#check Set.inter_empty
|
||||
|
||||
theorem emptyset_identity_ii (A : Set α)
|
||||
: A ∩ ∅ = ∅ := calc A ∩ ∅
|
||||
_ = { x | x ∈ A ∧ x ∈ ∅ } := rfl
|
||||
_ = { x | x ∈ A ∧ False } := rfl
|
||||
_ = { x | False } := by simp
|
||||
_ = ∅ := rfl
|
||||
|
||||
#check Set.inter_diff_self
|
||||
|
||||
theorem emptyset_identity_iii (A C : Set α)
|
||||
: A ∩ (C \ A) = ∅ := calc A ∩ (C \ A)
|
||||
_ = { x | x ∈ A ∧ x ∈ C \ A } := rfl
|
||||
_ = { x | x ∈ A ∧ (x ∈ C ∧ x ∉ A) } := rfl
|
||||
_ = { x | x ∈ C ∧ False } := by simp
|
||||
_ = { x | False } := by simp
|
||||
_ = ∅ := rfl
|
||||
|
||||
/-- #### Exercise 2.1
|
||||
|
||||
Assume that `A` is the set of integers divisible by `4`. Similarly assume that
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ namespace Enderton.Set.Chapter_3
|
|||
|
||||
If `x ∈ C` and `y ∈ C`, then `⟨x, y⟩ ∈ 𝒫 𝒫 C`.
|
||||
-/
|
||||
theorem theorem_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C)
|
||||
theorem lemma_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C)
|
||||
: OrderedPair x y ∈ 𝒫 𝒫 C := by
|
||||
have hxs : {x} ⊆ C := Set.singleton_subset_iff.mpr hx
|
||||
have hxys : {x, y} ⊆ C := Set.mem_mem_imp_pair_subset hx hy
|
||||
|
|
|
|||
|
|
@ -15,118 +15,118 @@
|
|||
\subsection{\verified{Arithmetic Series}}%
|
||||
\hyperlabel{sub:sum-arithmetic-series}
|
||||
|
||||
Let $(a_i)_{i \geq 0}$ be an arithmetic sequence with common difference $d$.
|
||||
Then for some $n \in \mathbb{N}$,
|
||||
\begin{equation}
|
||||
\hyperlabel{sub:sum-arithmetic-series-eq1}
|
||||
\sum_{i=0}^n a_i = \frac{(n + 1)(a_0 + a_n)}{2}.
|
||||
\end{equation}
|
||||
|
||||
\begin{proof}
|
||||
Let $(a_i)_{i \geq 0}$ be an arithmetic sequence with common difference $d$.
|
||||
Then for some $n \in \mathbb{N}$,
|
||||
\begin{equation}
|
||||
\hyperlabel{sub:sum-arithmetic-series-eq1}
|
||||
\sum_{i=0}^n a_i = \frac{(n + 1)(a_0 + a_n)}{2}.
|
||||
\end{equation}
|
||||
|
||||
\code{Common/Real/Sequence/Arithmetic}
|
||||
{Real.Arithmetic.sum\_recursive\_closed}
|
||||
|
||||
Let $(a_i)_{i \geq 0}$ be an arithmetic sequence with common difference $d$.
|
||||
By definition, for all $k \in \mathbb{N}$,
|
||||
\begin{equation}
|
||||
\hyperlabel{sub:sum-arithmetic-series-eq2}
|
||||
a_k = (a_0 + kd).
|
||||
\end{equation}
|
||||
Define predicate $P(n)$ as "identity \eqref{sub:sum-arithmetic-series-eq1}
|
||||
holds for value $n$."
|
||||
We use induction to prove $P(n)$ holds for all $n \geq 0$.
|
||||
\begin{proof}
|
||||
|
||||
\paragraph{Base Case}%
|
||||
Let $(a_i)_{i \geq 0}$ be an arithmetic sequence with common difference $d$.
|
||||
By definition, for all $k \in \mathbb{N}$,
|
||||
\begin{equation}
|
||||
\hyperlabel{sub:sum-arithmetic-series-eq2}
|
||||
a_k = (a_0 + kd).
|
||||
\end{equation}
|
||||
Define predicate $P(n)$ as "identity \eqref{sub:sum-arithmetic-series-eq1}
|
||||
holds for value $n$."
|
||||
We use induction to prove $P(n)$ holds for all $n \geq 0$.
|
||||
|
||||
Let $k = 0$.
|
||||
Then $$\sum_{i=0}^k a_i = a_0 = \frac{2a_0}{2} =
|
||||
\frac{(k + 1)(a_0 + a_k)}{2}.$$
|
||||
Therefore $P(0)$ holds.
|
||||
\paragraph{Base Case}%
|
||||
|
||||
\paragraph{Induction Step}%
|
||||
Let $k = 0$.
|
||||
Then $$\sum_{i=0}^k a_i = a_0 = \frac{2a_0}{2} =
|
||||
\frac{(k + 1)(a_0 + a_k)}{2}.$$
|
||||
Therefore $P(0)$ holds.
|
||||
|
||||
Assume induction hypothesis $P(k)$ holds for some $k \geq 0$.
|
||||
Then
|
||||
\begin{align*}
|
||||
\sum_{i=0}^{k+1} a_i
|
||||
& = \sum_{i=0}^k a_i + a_{k+1} \\
|
||||
& = \frac{(k + 1)(a_0 + a_k)}{2} + a_{k+1}
|
||||
& \text{induction hypothesis} \\
|
||||
& = \frac{(k + 1)(a_0 + (a_0 + kd))}{2} + (a_0 + (k + 1)d)
|
||||
& \eqref{sub:sum-arithmetic-series-eq2} \\
|
||||
& = \frac{(k + 1)(2a_0 + kd)}{2} + (a_0 + (k + 1)d) \\
|
||||
& = \frac{(k + 1)(2a_0 + kd) + 2a_0 + 2(k + 1)d}{2} \\
|
||||
& = \frac{2ka_0 + k^2d + 4a_0 + kd + 2kd + 2d}{2} \\
|
||||
& = \frac{(k + 2)(2a_0 + kd + d)}{2} \\
|
||||
& = \frac{(k + 2)(a_0 + a_0 + (k + 1)d)}{2} \\
|
||||
& = \frac{(k + 2)(a_0 + a_{k+1})}{2}
|
||||
& \eqref{sub:sum-arithmetic-series-eq2} \\
|
||||
& = \frac{((k + 1) + 1)(a_0 + a_{k+1})}{2}.
|
||||
\end{align*}
|
||||
Thus $P(k)$ implies $P(k + 1)$ holds true.
|
||||
\paragraph{Induction Step}%
|
||||
|
||||
\paragraph{Conclusion}%
|
||||
Assume induction hypothesis $P(k)$ holds for some $k \geq 0$.
|
||||
Then
|
||||
\begin{align*}
|
||||
\sum_{i=0}^{k+1} a_i
|
||||
& = \sum_{i=0}^k a_i + a_{k+1} \\
|
||||
& = \frac{(k + 1)(a_0 + a_k)}{2} + a_{k+1}
|
||||
& \text{induction hypothesis} \\
|
||||
& = \frac{(k + 1)(a_0 + (a_0 + kd))}{2} + (a_0 + (k + 1)d)
|
||||
& \eqref{sub:sum-arithmetic-series-eq2} \\
|
||||
& = \frac{(k + 1)(2a_0 + kd)}{2} + (a_0 + (k + 1)d) \\
|
||||
& = \frac{(k + 1)(2a_0 + kd) + 2a_0 + 2(k + 1)d}{2} \\
|
||||
& = \frac{2ka_0 + k^2d + 4a_0 + kd + 2kd + 2d}{2} \\
|
||||
& = \frac{(k + 2)(2a_0 + kd + d)}{2} \\
|
||||
& = \frac{(k + 2)(a_0 + a_0 + (k + 1)d)}{2} \\
|
||||
& = \frac{(k + 2)(a_0 + a_{k+1})}{2}
|
||||
& \eqref{sub:sum-arithmetic-series-eq2} \\
|
||||
& = \frac{((k + 1) + 1)(a_0 + a_{k+1})}{2}.
|
||||
\end{align*}
|
||||
Thus $P(k)$ implies $P(k + 1)$ holds true.
|
||||
|
||||
By mathematical induction, it follows for all $n \geq 0$, $P(n)$ is true.
|
||||
\paragraph{Conclusion}%
|
||||
|
||||
\end{proof}
|
||||
By mathematical induction, it follows for all $n \geq 0$, $P(n)$ is true.
|
||||
|
||||
\end{proof}
|
||||
|
||||
\subsection{\verified{Geometric Series}}%
|
||||
\hyperlabel{sub:sum-geometric-series}
|
||||
|
||||
Let $(a_i)_{i \geq 0}$ be a geometric sequence with common ratio $r \neq 1$.
|
||||
Then for some $n \in \mathbb{N}$,
|
||||
\begin{equation}
|
||||
\hyperlabel{sub:sum-geometric-series-eq1}
|
||||
\sum_{i=0}^n a_i = \frac{a_0(1 - r^{n+1})}{1 - r}.
|
||||
\end{equation}
|
||||
|
||||
\begin{proof}
|
||||
Let $(a_i)_{i \geq 0}$ be a geometric sequence with common ratio $r \neq 1$.
|
||||
Then for some $n \in \mathbb{N}$,
|
||||
\begin{equation}
|
||||
\hyperlabel{sub:sum-geometric-series-eq1}
|
||||
\sum_{i=0}^n a_i = \frac{a_0(1 - r^{n+1})}{1 - r}.
|
||||
\end{equation}
|
||||
|
||||
\code{Common/Real/Sequence/Geometric}
|
||||
{Real.Geometric.sum\_recursive\_closed}
|
||||
|
||||
Let $(a_i)_{i \geq 0}$ be a geometric sequence with common ratio $r \neq 1$.
|
||||
By definition, for all $k \in \mathbb{N}$,
|
||||
\begin{equation}
|
||||
\hyperlabel{sub:sum-geometric-series-eq2}
|
||||
a_k = a_0r^k.
|
||||
\end{equation}
|
||||
Define predicate $P(n)$ as "identity \eqref{sub:sum-geometric-series-eq1}
|
||||
holds for value $n$."
|
||||
We use induction to prove $P(n)$ holds for all $n \geq 0$.
|
||||
\begin{proof}
|
||||
|
||||
\paragraph{Base Case}%
|
||||
Let $(a_i)_{i \geq 0}$ be a geometric sequence with common ratio $r \neq 1$.
|
||||
By definition, for all $k \in \mathbb{N}$,
|
||||
\begin{equation}
|
||||
\hyperlabel{sub:sum-geometric-series-eq2}
|
||||
a_k = a_0r^k.
|
||||
\end{equation}
|
||||
Define predicate $P(n)$ as "identity \eqref{sub:sum-geometric-series-eq1}
|
||||
holds for value $n$."
|
||||
We use induction to prove $P(n)$ holds for all $n \geq 0$.
|
||||
|
||||
Let $k = 0$.
|
||||
Then $$\sum_{i=0}^k a_i = a_0 = \frac{a_0(1 - r)}{1 - r} =
|
||||
\frac{a_0(1 - r^{k+1})}{1 - r}$$
|
||||
Therefore $P(0)$ holds.
|
||||
\paragraph{Base Case}%
|
||||
|
||||
\paragraph{Induction Step}%
|
||||
Let $k = 0$.
|
||||
Then $$\sum_{i=0}^k a_i = a_0 = \frac{a_0(1 - r)}{1 - r} =
|
||||
\frac{a_0(1 - r^{k+1})}{1 - r}$$
|
||||
Therefore $P(0)$ holds.
|
||||
|
||||
Assume induction hypothesis $P(k)$ holds for some $k \geq 0$.
|
||||
Then
|
||||
\begin{align*}
|
||||
\sum_{i=0}^{k+1} a_i
|
||||
& = \sum_{i=0}^k a_i + a_{k+1} \\
|
||||
& = \frac{a_0(1 - r^{k+1})}{1 - r} + a_{k + 1}
|
||||
& \text{induction hypothesis} \\
|
||||
& = \frac{a_0(1 - r^{k+1})}{1 - r} + a_0r^{k + 1}
|
||||
& \eqref{sub:sum-geometric-series-eq2} \\
|
||||
& = \frac{a_0(1 - r^{k+1}) + a_0r^{k+1}(1 - r)}{1 - r} \\
|
||||
& = \frac{a_0(1 - r^{k+1} + r^{k+1}(1 - r))}{1 - r} \\
|
||||
& = \frac{a_0(1 - r^{k+1} + r^{k+1} - r^{k+2})}{1 - r} \\
|
||||
& = \frac{a_0(1 - r^{k+2})}{1 - r} \\
|
||||
& = \frac{a_0(1 - r^{(k + 1) + 1})}{1 - r}.
|
||||
\end{align*}
|
||||
Thus $P(k)$ implies $P(k + 1)$ holds true.
|
||||
\paragraph{Induction Step}%
|
||||
|
||||
\paragraph{Conclusion}%
|
||||
Assume induction hypothesis $P(k)$ holds for some $k \geq 0$.
|
||||
Then
|
||||
\begin{align*}
|
||||
\sum_{i=0}^{k+1} a_i
|
||||
& = \sum_{i=0}^k a_i + a_{k+1} \\
|
||||
& = \frac{a_0(1 - r^{k+1})}{1 - r} + a_{k + 1}
|
||||
& \text{induction hypothesis} \\
|
||||
& = \frac{a_0(1 - r^{k+1})}{1 - r} + a_0r^{k + 1}
|
||||
& \eqref{sub:sum-geometric-series-eq2} \\
|
||||
& = \frac{a_0(1 - r^{k+1}) + a_0r^{k+1}(1 - r)}{1 - r} \\
|
||||
& = \frac{a_0(1 - r^{k+1} + r^{k+1}(1 - r))}{1 - r} \\
|
||||
& = \frac{a_0(1 - r^{k+1} + r^{k+1} - r^{k+2})}{1 - r} \\
|
||||
& = \frac{a_0(1 - r^{k+2})}{1 - r} \\
|
||||
& = \frac{a_0(1 - r^{(k + 1) + 1})}{1 - r}.
|
||||
\end{align*}
|
||||
Thus $P(k)$ implies $P(k + 1)$ holds true.
|
||||
|
||||
By mathematical induction, it follows for all $n \geq 0$, $P(n)$ is true.
|
||||
\paragraph{Conclusion}%
|
||||
|
||||
\end{proof}
|
||||
By mathematical induction, it follows for all $n \geq 0$, $P(n)$ is true.
|
||||
|
||||
\end{proof}
|
||||
|
||||
\end{document}
|
||||
|
|
|
|||
50
preamble.tex
50
preamble.tex
|
|
@ -44,61 +44,47 @@
|
|||
\label{#1}%
|
||||
\hypertarget{#1}{}}
|
||||
|
||||
% Denote whether we are working with a standard/Mathlib statement (lean) or a
|
||||
% custom one (code).
|
||||
% Denote if working with a predefined statement/theorem or a custom one.
|
||||
\newcommand\@leanlink[4]{%
|
||||
\textcolor{blue}{\raisebox{-4.5pt}{%
|
||||
\tikz{\draw (0, 0) node[yscale=-1,xscale=1] {\faFont};}}}%
|
||||
{-\;}\href{#1/#2.html\##3}{#4}}
|
||||
|
||||
\textcolor{BlueViolet}{\raisebox{-4.5pt}{%
|
||||
\tikz{\draw (0, 0) node[yscale=-1,xscale=1] {\faFont};}}{-\;}}%
|
||||
\href{#1/#2.html\##3}{\color{BlueViolet}{#4}}}
|
||||
\newcommand\@codelink[4]{%
|
||||
\textcolor{blue}{\raisebox{-4.5pt}{%
|
||||
\tikz{\draw (0, 0) node[] {\faCodeBranch};}}}%
|
||||
{-\;}\href{#1/#2.html\##3}{#4}}
|
||||
\textcolor{MidnightBlue}{\raisebox{-4.5pt}{%
|
||||
\tikz{\draw (0, 0) node[xshift=8pt] {\faCodeBranch};}}{-\;}}%
|
||||
\href{#1/#2.html\##3}{\color{MidnightBlue}{#4}}}
|
||||
|
||||
% Reference to an anchor of Lean documentation.
|
||||
% Reference to an anchor of generated Lean documentation.
|
||||
\newcommand\leanref[3]{%
|
||||
\@leanlink{#1}{#2}{#3}{#3}\vspace{10pt}}
|
||||
\WithSuffix\newcommand\leanref*[3]{%
|
||||
\@leanlink{#1}{#2}{#3}{#3}}
|
||||
|
||||
\newcommand\coderef[3]{%
|
||||
\@codelink{#1}{#2}{#3}{#3}\vspace{10pt}}
|
||||
\WithSuffix\newcommand\coderef*[3]{%
|
||||
\@codelink{#1}{#2}{#3}{#3}}
|
||||
|
||||
% Variants that allows customizing display text.
|
||||
\newcommand\leanpref[4]{%
|
||||
\@leanlink{#1}{#2}{#3}{#4}\vspace{10pt}}
|
||||
\WithSuffix\newcommand\leanpref*[4]{%
|
||||
\@leanlink{#1}{#2}{#3}{#4}}
|
||||
|
||||
\newcommand\codepref[4]{%
|
||||
\@codelink{#1}{#2}{#3}{#4}\vspace{10pt}}
|
||||
\WithSuffix\newcommand\codepref*[4]{%
|
||||
\@codelink{#1}{#2}{#3}{#4}}
|
||||
|
||||
% Macro to build all Lean related commands relative to a specified directory.
|
||||
\newcommand\makeleancommands[1]{%
|
||||
\newcommand\lean[2]{%
|
||||
\leanref{#1}{##1}{##2}}
|
||||
\noindent\leanref{#1}{##1}{##2}}
|
||||
\WithSuffix\newcommand\lean*[2]{%
|
||||
\leanref*{#1}{##1}{##2}}
|
||||
\vspace{6pt}\noindent\leanref{#1}{##1}{##2}}
|
||||
|
||||
\newcommand\code[2]{%
|
||||
\coderef{#1}{##1}{##2}}
|
||||
\noindent\coderef{#1}{##1}{##2}}
|
||||
\WithSuffix\newcommand\code*[2]{%
|
||||
\coderef*{#1}{##1}{##2}}
|
||||
\vspace{6pt}\noindent\coderef{#1}{##1}{##2}}
|
||||
|
||||
\newcommand\leanp[3]{%
|
||||
\leanpref{#1}{##1}{##2}{##3}}
|
||||
\noindent\leanpref{#1}{##1}{##2}{##3}}
|
||||
\WithSuffix\newcommand\leanp*[3]{%
|
||||
\leanpref*{#1}{##1}{##2}{##3}}
|
||||
\vspace{6pt}\noindent\leanpref{#1}{##1}{##2}{##3}}
|
||||
|
||||
\newcommand\codep[3]{%
|
||||
\codepref{#1}{##1}{##2}{##3}}
|
||||
\noindent\codepref{#1}{##1}{##2}{##3}}
|
||||
\WithSuffix\newcommand\codep*[3]{%
|
||||
\codepref*{#1}{##1}{##2}{##3}}
|
||||
\vspace{6pt}\noindent\codepref{#1}{##1}{##2}{##3}}
|
||||
}
|
||||
|
||||
% ========================================
|
||||
|
|
@ -124,11 +110,7 @@
|
|||
|
||||
\newcommand\@statement[1]{%
|
||||
\linedivider*\paragraph{\normalfont\normalsize\textit{#1.}}}
|
||||
\newcommand{\statementpadding}{\ \vspace{8pt}}
|
||||
|
||||
\newenvironment{answer}{\@statement{Answer}}{\hfill$\square$}
|
||||
\newenvironment{axiom}{\@statement{Axiom}}{\hfill$\square$}
|
||||
\newenvironment{definition}{\@statement{Definition}}{\hfill$\square$}
|
||||
\renewenvironment{proof}{\@statement{Proof}}{\hfill$\square$}
|
||||
|
||||
\newtheorem{corollaryinner}{Corollary}
|
||||
|
|
|
|||
Loading…
Reference in New Issue