From 99dcc64b34775b724e9a838a2cc69f034a2828e9 Mon Sep 17 00:00:00 2001
From: KellyJDavis <kdavis@alum.mit.edu>
Date: Fri, 17 Jul 2026 14:37:17 +0200
Subject: [PATCH] Fixed Lean4 reference

---
 blueprint/src/sections/sec10/10-2_spacetime.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/blueprint/src/sections/sec10/10-2_spacetime.tex b/blueprint/src/sections/sec10/10-2_spacetime.tex
index 41babb4..bda157f 100644
--- a/blueprint/src/sections/sec10/10-2_spacetime.tex
+++ b/blueprint/src/sections/sec10/10-2_spacetime.tex
@@ -588,7 +588,7 @@ \section{Spacetime}\label{sctn:spacetime}
 
 \begin{lemma}[No-Diamond Points Have Only the Whole Space as Neighbourhood]
     \label{lmm:alexandrov-nbhd-univ-of-no-diamond}
-    \lean{alexandrov_nbhd_univ_of_no_diamond}
+    \lean{Physicslib4.Spacetime.alexandrov_nbhd_univ_of_no_diamond}
     \leanfile{Physicslib4/Spacetime/Causality.lean}
     \uses{def:alexandrov-topology}
     \leanok