summaryrefslogtreecommitdiff
path: root/library/set
diff options
context:
space:
mode:
authoradelon <22380201+adelon@users.noreply.github.com>2024-05-23 13:11:39 +0200
committeradelon <22380201+adelon@users.noreply.github.com>2024-05-23 13:11:39 +0200
commit091da55df4de2d27697203fdddcdacd3c713b38c (patch)
tree2a2958d2e5ffd822a916c56dc515eb396f77971e /library/set
parent9113b4fddb67e5a101e4a26ead3d1d1bf72664ce (diff)
Update formatting
Diffstat (limited to 'library/set')
-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}