From 7b1308fb1e7e00efcce535cb42e26009c27dbc3c Mon Sep 17 00:00:00 2001
From: Patrick Massot <patrickmassot@free.fr>
Date: Fri, 24 May 2024 10:52:03 -0400
Subject: [PATCH] Fix Lean names in blueprint

---
 blueprint/src/global_convex_integration.tex | 6 +++---
 blueprint/src/local_convex_integration.tex  | 8 ++++----
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/blueprint/src/global_convex_integration.tex b/blueprint/src/global_convex_integration.tex
index 70f31df2..ef09508a 100644
--- a/blueprint/src/global_convex_integration.tex
+++ b/blueprint/src/global_convex_integration.tex
@@ -366,7 +366,7 @@ \subsection{Jets spaces}
 \begin{definition}
 \label{def:holonomic_section}
 \leanok
-\lean{OneJetSet.IsHolonomicAt, OneJetSec.isHolonomicAt_iff}
+\lean{OneJetSec.IsHolonomicAt, OneJetSec.isHolonomicAt_iff}
 \uses{def:one_jet_space}
 A section $\F$ of $J^1(M, N) → M$ is called holonomic if it is the
 $1$--jet of its base map.
@@ -520,7 +520,7 @@ \subsection*{Parametricity for free}
   \label{lem:param_for_free}
   \uses{def:h-princ}
   \leanok
-  \lean{RelMfld.SatisfiesHPrinciple.SatisfiesHPrincipleWith}
+  \lean{RelMfld.SatisfiesHPrinciple.satisfiesHPrincipleWith}
   Let $\Rel$ be a first order differential relation for maps from $M$ to
   $N$.
   If, for every manifold with boundary $P$, $\Rel^P$ satisfies the
@@ -631,7 +631,7 @@ \section{The $h$-principle for open and ample differential relations}
   \label{thm:open_ample}
   % \uses{def:h-princ} % causes transitive arrow in depgraph
   \leanok
-  \lean{RelMfld.Ample.SatisfiesHPrincipleWith}
+  \lean{RelMfld.Ample.satisfiesHPrincipleWith}
   For any manifolds $X$ and $Y$, any relation $\Rel ⊂ J^1(X, Y)$ that is open
   and ample satisfies the full $h$-principle (relative, parametric and $C^0$-dense).
 \end{theorem}
diff --git a/blueprint/src/local_convex_integration.tex b/blueprint/src/local_convex_integration.tex
index 9f671dd6..f0f720c7 100644
--- a/blueprint/src/local_convex_integration.tex
+++ b/blueprint/src/local_convex_integration.tex
@@ -101,7 +101,7 @@ \section{The main inductive step}
 \begin{definition}
   \label{def:hol_partial}
   \leanok
-  \lean{JetSet.IsPartHolonomicAt}
+  \lean{JetSec.IsPartHolonomicAt}
   Let $E'$ be a linear subspace of $E$.
   A map $\F = (f, φ) : E → F × \Hom(E, F)$ is $E'$--holonomic if,
   for every $v$ in $E'$ and every $x$, $Df(x)v = φ(x)v$.
@@ -134,7 +134,7 @@ \section{The main inductive step}
 \begin{definition}
   \label{def:htpy_jet_sec_loc}
   \leanok
-  \lean{htpy_jet_sec}
+  \lean{HtpyJetSec}
   A $1$-jet section from $E$ to $F$ is a function from $E$ to $F × \Hom(E, F)$.
   A homotopy of $1$-jet sections is a smooth map
   $\F : ℝ × E → F × \Hom(E, F)$.
@@ -327,7 +327,7 @@ \section{Ample differential relations}
 \begin{lemma}
   \label{lem:ample_codim_two}
   \uses{def:ample_subset}
-  \lean{ample_of_two_le_codim}
+  \lean{AmpleSet.of_one_lt_codim}
   \leanok
   The complement of a linear subspace of codimension at least 2 is
   ample.
@@ -369,7 +369,7 @@ \section{Ample differential relations}
 \begin{definition}
   \label{def:ample_relation_loc}
   \leanok
-  \lean{RelLoc.isAmple}
+  \lean{RelLoc.IsAmple}
   \uses{def:ample_subset, def:rel_slice}
   A first order differential relation $\Rel$ is ample if all its slices
   are ample.