summaryrefslogtreecommitdiff
path: root/library/everything.tex
diff options
context:
space:
mode:
authoradelon <22380201+adelon@users.noreply.github.com>2025-07-02 20:28:22 +0200
committerGitHub <noreply@github.com>2025-07-02 20:28:22 +0200
commit793849dd0b20bc70ea0e0ecfd5008a3806eca0d9 (patch)
tree280949f358a695c5471212cc5b22950399d8cd57 /library/everything.tex
parent3caadfbe0fdb417b8edebc17002ddafe795a4bcc (diff)
parent8fd49ae84e8cc4524c19b20fa0aabb4e77a46cd5 (diff)
Merge pull request #2 from Simon-Kor/main
Merge (finally)
Diffstat (limited to 'library/everything.tex')
-rw-r--r--library/everything.tex8
1 files changed, 7 insertions, 1 deletions
diff --git a/library/everything.tex b/library/everything.tex
index 61bccb2..94dd6d8 100644
--- a/library/everything.tex
+++ b/library/everything.tex
@@ -16,12 +16,13 @@
\import{relation/uniqueness.tex}
\import{function.tex}
\import{ordinal.tex}
-%\import{nat.tex}
+\import{nat.tex}
\import{cardinal.tex}
\import{algebra/magma.tex}
\import{algebra/semigroup.tex}
\import{algebra/monoid.tex}
\import{algebra/group.tex}
+
\import{order/order.tex}
%\import{order/semilattice.tex}
\import{topology/topological-space.tex}
@@ -29,7 +30,12 @@
\import{topology/disconnection.tex}
\import{topology/separation.tex}
\import{numbers.tex}
+\import{topology/urysohn2.tex}
\begin{proposition}\label{trivial}
$x = x$.
\end{proposition}
+
+\begin{proposition}\label{safe}
+ Contradiction.
+\end{proposition}