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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
|
\import{set.tex}
\begin{proposition}\label{times_subseteq_left}
Suppose $A\subseteq C$. Then $A\times B\subseteq C\times B$.
\end{proposition}
\begin{proof}
We have for all $w\in A\times B$ we have $w\in C\times B$
by \cref{subseteq,times}.
Follows by \cref{subseteq}.
\end{proof}
\begin{proposition}\label{times_subseteq_right}
Suppose $B\subseteq D$. Then $A\times B\subseteq A\times D$.
\end{proposition}
\begin{proof}
We have for all $w\in A\times B$ we have $w\in A\times D$
by \cref{subseteq,times}.
Follows by \cref{subseteq}.
\end{proof}
\begin{proposition}\label{inter_times_intro}
Suppose $w\in(A\inter B)\times (C\inter D)$.
Then $w\in(A\times C)\inter (B\times D)$.
\end{proposition}
\begin{proof}
Take $a,c$ such that $w = (a, c)$
by \cref{times_elem_is_tuple}.
Then $a\in A, B$ and $c\in C,D$
by \cref{times_tuple_elim,inter}.
Thus $w\in (A\times C), (B\times D)$.
\end{proof}
\begin{proposition}\label{inter_times_elim}
Suppose $w\in(A\times C)\inter (B\times D)$.
Then $w\in(A\inter B)\times (C\inter D)$.
\end{proposition}
\begin{proof}
$w\in A\times C$.
Take $a, c$ such that $w = (a, c)$.
$a\in A, B$ by \cref{inter,times_tuple_elim}.
$c\in C, D$ by \cref{inter,times_tuple_elim}.
Thus $(a,c) \in (A\inter B)\times (C\inter D)$ by \cref{times,inter_intro}.
\end{proof}
\begin{proposition}\label{inter_times}
$(A\inter B)\times (C\inter D) = (A\times C)\inter (B\times D)$.
\end{proposition}
\begin{proof}
Follows by \cref{setext,inter_times_intro,inter_times_elim}.
\end{proof}
\begin{proposition}\label{inter_times_right}
$(X\inter Y)\times Z = (X\times Z)\inter (Y\times Z)$.
\end{proposition}
\begin{proof}
Follows by \cref{inter_times,inter_idempotent}.
\end{proof}
\begin{proposition}\label{inter_times_left}
$X\times (Y\inter Z) = (X\times Y)\inter (X\times Z)$.
\end{proposition}
\begin{proof}
Follows by \cref{inter_times,inter_idempotent}.
\end{proof}
\begin{proposition}\label{union_times_intro}
Suppose $w\in(A\union B)\times (C\union D)$.
Then $w\in(A\times C)\union (B\times D)\union (A\times D)\union (B\times C)$.
\end{proposition}
\begin{proof}
Take $a,c$ such that $w = (a, c)$
by \cref{times_elem_is_tuple,union_iff}.
$a\in A$ or $a\in B$ by \cref{union_iff,times_tuple_elim}.
$c\in C$ or $c\in D$ by \cref{union_iff,times_tuple_elim}.
Thus $(a, c)\in (A\times C)$ or $(a, c)\in (B\times D)$ or $(a, c)\in (A\times D)$ or $(a, c)\in (B\times C)$.
Thus $(a, c)\in (A\times C)\union (B\times D)\union (A\times D)\union (B\times C)$.
\end{proof}
\begin{proposition}\label{union_times_elim}
Suppose $w\in(A\times C)\union (B\times D)\union (A\times D)\union (B\times C)$.
Then $w\in(A\union B)\times (C\union D)$.
\end{proposition}
\begin{proof}
Take $a,c$ such that $w = (a,c)$
by \cref{times_elem_is_tuple,union_iff}.
We have $a\in A$ or $a\in B$
by \cref{times_tuple_elim,union_iff}.
We have $c\in C$ or $c\in D$
by \cref{times_tuple_elim,union_iff}.
Thus $a\in A\union B$ and $c\in C\union D$ by \cref{union_iff}.
Follows by \cref{times_tuple_intro}.
\end{proof}
\begin{proposition}\label{union_times}
$(A\union B)\times (C\union D) = (A\times C)\union (B\times D)\union (A\times D)\union (B\times C)$.
\end{proposition}
\begin{proof}
Follows by \cref{setext,union_times_intro,union_times_elim}.
\end{proof}
\begin{proposition}\label{union_times_left}
$(X\union Y)\times Z = (X\times Z)\union (Y\times Z)$.
\end{proposition}
\begin{proof}
Follows by \cref{union_times,union_idempotent,union_assoc}.
\end{proof}
\begin{proposition}\label{union_times_right}
$X\times (Y\union Z) = (X\times Y)\union (X\times Z)$.
\end{proposition}
\begin{proof}
Follows by \cref{union_times,union_idempotent,union_assoc,union_comm}.
\end{proof}
|
