From cfd5061ced34f061e84ecca2a266f8f4cd01ce36 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 30 Apr 2024 12:26:13 +0200
Subject: Adding the first formalisation of reals

---
 library/everything.tex | 1 +
 1 file changed, 1 insertion(+)

(limited to 'library/everything.tex')

diff --git a/library/everything.tex b/library/everything.tex
index a5166af..61bccb2 100644
--- a/library/everything.tex
+++ b/library/everything.tex
@@ -28,6 +28,7 @@
 \import{topology/basis.tex}
 \import{topology/disconnection.tex}
 \import{topology/separation.tex}
+\import{numbers.tex}
 
 \begin{proposition}\label{trivial}
     $x = x$.
-- 
cgit v1.2.3