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 --- latex/stdlib.tex | 1 + 1 file changed, 1 insertion(+) (limited to 'latex/stdlib.tex') diff --git a/latex/stdlib.tex b/latex/stdlib.tex index e545395..dba42a2 100644 --- a/latex/stdlib.tex +++ b/latex/stdlib.tex @@ -45,4 +45,5 @@ \input{../library/topology/topological-space.tex} \input{../library/topology/basis.tex} \input{../library/topology/disconnection.tex} + \input{../library/numbers.tex} \end{document} -- cgit v1.2.3