Re: [isabelle] New in the AFP: Formal Puiseux Series



> Lean does seem to have "manifolds with corners":
> https://leanprover-community.github.io/mathlib_docs/geometry/manifold/smooth_manifold_with_corners.html
>
> Perhaps you could ask Sébastien Gouëzel (who did it) on his perspective
> on this. I hear he also has a soft spot for Isabelle. :)

You are right, we should probably ask him. A quick review of that page suggest they did not solve the problem we are discussing though, i.e. defining integrals on such manifolds and using partition of unities arguments to reason about them.

Mohammad





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.