Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2,569 research declarations. Search 10,000 more complete Mathlib declarations.
2569 results
RelLoc.FormalSol.improve
Plain-language statement
Homotopy of formal solutions obtained by successive corrugations in some landscape L to improve a formal solution 𝓕 until it becomes holonomic near L.K₀.
Source project: Sphere eversion
Person-level attribution pending.
RelLoc.HtpyFormalSol.exists_sol
Plain-language statement
A corollary of the local parametric h-principle, forgetting the homotopy and ε-closeness, and just stating the existence of a solution that is holonomic near K. Furthermore, we assume that P = ℝ and K is of the form compact set × I. This is sufficient to prove sphere eversion.
Source project: Sphere eversion
Person-level attribution pending.
RelMfld.Ample.localize
Plain-language statement
Ampleness survives localization
Source project: Sphere eversion
Person-level attribution pending.
RelMfld.Ample.satisfiesHPrincipleWith
Plain-language statement
Gromov's Theorem
Source project: Sphere eversion
Person-level attribution pending.
RelMfld.SatisfiesHPrincipleWith.bs
Plain-language statement
If a relation satisfies the parametric relative C⁰-dense h-principle wrt some data then we can forget the homotopy and get a family of solutions from every family of formal solutions.
Source project: Sphere eversion
Person-level attribution pending.
Rep.herbrandQuotient_isNonarchimedeanLocalField_units
Plain-language statement
herbrand quotient of Lˣ is [L:K]
Source project: Class Field Theory
Person-level attribution pending.