From 5487c1421a7894567e0b211f505f4b6c97edec73 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Tue, 6 Feb 2024 11:34:57 +0100 Subject: [PATCH] Fix comment typo from the port; ought to regenerate the blueprint. --- SphereEversion/Local/AmpleSet.lean | 2 +- blueprint/src/local_convex_integration.tex | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/SphereEversion/Local/AmpleSet.lean b/SphereEversion/Local/AmpleSet.lean index 9d6e02a6..4d28c645 100644 --- 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 index bc7e7fb2..0ec18244 100644 --- 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}