PatrickMassot / leanblueprint

plasTeX plugin to build formalization blueprints.
Apache License 2.0
163 stars 26 forks source link

small error in the latex example #54

Open ouboub opened 1 week ago

ouboub commented 1 week ago

Hi this is a very minor thing but

\begin{theorem}[Smale 1958]
  \label{thm:sphere_eversion}
  \lean{sphere_eversion}
  \leanok
  \uses{def:immersion}
  There is a homotopy of immersions of $𝕊^2$ into $ℝ^3$ from the inclusion map to
  the antipodal map $a : q ↦ -q$.
\end{theorem}

\begin{proof}
  \leanok
  \uses{thm:open_ample, lem:open_ample_immersion}
  This obviously follows from what we did so far.
\end

should be

\begin{theorem}[Smale 1958]
  \label{thm:sphere_eversion}
  \lean{sphere_eversion}
  \leanok
  \uses{def:immersion}
  There is a homotopy of immersions of $𝕊^2$ into $ℝ^3$ from the inclusion map to
  the antipodal map $a : q ↦ -q$.
\end{theorem}

\begin{proof}
  \leanok
  \uses{thm:open_ample, lem:open_ample_immersion}
  This obviously follows from what we did so far.
\end{proof}
utensil commented 1 week ago

For others reading this issue, the issue spotted here seems to be that the \end{proof} was typed as \end.

ouboub commented 5 days ago

For others reading this issue, the issue spotted here seems to be that the \end{proof} was typed as \end.

I copied that example from https://github.com/PatrickMassot/leanblueprint

So the errors is theirs, and still, persists, I recommend correcting it on that page

utensil commented 5 days ago

You are welcome to send a PR~

ouboub commented 5 days ago

You are welcome to send a PR~

Done