Fix comment typo from the port; ought to regenerate the blueprint.

leanprover-community · Feb 6, 2024 · 5487c14 · 5487c14
1 parent 5c609a5
commit 5487c14
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/SphereEversion/Local/AmpleSet.lean b/SphereEversion/Local/AmpleSet.lean
@@ -67,7 +67,7 @@ theorem AmpleSet.preimage {s : Set F} (h : AmpleSet s) (L : E ≃L[ℝ] F) : Amp
 open scoped Pointwise
 
 /-- Translating a ample set is ample.
-We basically mimic `ample_set.image`. We could prove the common generalization using
+We basically mimic `AmpleSet.image`. We could prove the common generalization using
 continuous affine equivalences -/
 theorem AmpleSet.vadd [ContinuousAdd E] {s : Set E} (h : AmpleSet s) {y : E} :
     AmpleSet (y +ᵥ s) := by

diff --git a/blueprint/src/local_convex_integration.tex b/blueprint/src/local_convex_integration.tex
@@ -319,7 +319,7 @@ \section{Ample differential relations}
 \begin{definition}
   \label{def:ample_subset}
   \leanok
-  \lean{ample_set}
+  \lean{AmpleSet}
   A subset $Ω$ of a real vector space $E$ is ample if the convex
   hull of each connected component of $Ω$ is the whole $E$.
 \end{definition}