summaryrefslogtreecommitdiff
path: root/library/set/powerset.tex
diff options
context:
space:
mode:
Diffstat (limited to 'library/set/powerset.tex')
-rw-r--r--library/set/powerset.tex5
1 files changed, 2 insertions, 3 deletions
diff --git a/library/set/powerset.tex b/library/set/powerset.tex
index 80da4cb..7f30f68 100644
--- a/library/set/powerset.tex
+++ b/library/set/powerset.tex
@@ -6,8 +6,7 @@
The powerset of $X$ denotes $\pow{X}$.
\end{abbreviation}
-\begin{axiom}%
-\label{pow_iff}
+\begin{axiom}\label{pow_iff}
$B\in\pow{A}$ iff $B\subseteq A$.
\end{axiom}
@@ -76,7 +75,7 @@
% LATER
%\begin{proposition}\label{powerset_cons}
-% Then $\pow{\cons{b}{A}} = \pow{A}\union \{\cons{b}{B}\mid B\in\pow{A}\}$.
+% $\pow{\cons{b}{A}} = \pow{A}\union \{\cons{b}{B}\mid B\in\pow{A}\}$.
%\end{proposition}
\begin{proposition}\label{powerset_union_subseteq}