blob: 40f93434241a62b894b1e630b23a72b01fc40eab (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
|
\begin{proposition}\label{suffices_exact}
Let $A$ be a set.
$A=A$.
\end{proposition}
\begin{proof}
It suffices to show that $A=A\land A=A$.
Follows.
\end{proof}
\begin{proposition}\label{calculation_equality_exact}
Let $A$ be a set.
Suppose $A=\emptyset\land \emptyset=\{A\}$.
Then $A=\{A\}$.
\end{proposition}
\begin{proof}
\begin{align*}
A
&= \emptyset
\explanation{by \cref{suffices_exact}}
\\
&= \{A\}
\explanation{by assumption}
\end{align*}
Follows by assumption.
\end{proof}
\begin{proposition}\label{calculation_biconditional_exact}
Let $A$ be a set.
$(A=A)\iff ((A=A)\lor(A\neq A))$.
\end{proposition}
\begin{proof}
\begin{align*}
A=A
&\iff \top
\\
&\iff (A=A)\lor(A\neq A)
\explanation{by assumption}
\end{align*}
Follows by assumption.
\end{proof}
\begin{proposition}\label{calculation_quantified_exact}
Let $A$ be a set.
For all $x,y\in A$ such that $x=y$ we have $x=y$.
\end{proposition}
\begin{proof}
For all $x,y\in A$ such that $x=y$, we have
\begin{align*}
x
&= y
\end{align*}
Follows by assumption.
\end{proof}
\begin{proposition}\label{since_structural_exact}
Let $A$ be a set.
Suppose $A=A$.
Then $A=A$.
\end{proposition}
\begin{proof}
Since $A=A$, we have $A=A$ by assumption.
Follows by assumption.
\end{proof}
\begin{proposition}\label{since_discharge_exact}
Let $A,B$ be sets.
Suppose $A=A$.
Then $A=A$.
\end{proposition}
\begin{proof}
Since $B=B$, we have $A=A$ by assumption.
Follows by assumption.
\end{proof}
\begin{proposition}\label{suffices_omitted_exact}
Let $A$ be a set.
$A=A$.
\end{proposition}
\begin{proof}
It suffices to show that $A=A$.
Omitted.
\end{proof}
|
