Per corrugation
per_corrugation
Plain-language statement
The integral appearing in corrugations is periodic.
Source project: Sphere eversion
Person-level attribution pending.
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 22 research declarations. Search 10,000 more complete Mathlib declarations.
22 results
Clear filtersper_corrugation
Plain-language statement
The integral appearing in corrugations is periodic.
Source project: Sphere eversion
Person-level attribution pending.
relative_inductive_construction_of_loc
Plain-language statement
We are given a suitably nice extended metric space X and three local constraints P₀,P₀' and P₁ on maps from X to some type Y. All maps entering the discussion are required to statisfy P₀ everywhere. The goal is to turn a map f₀ satisfying P₁ near a compact set K into one satisfying everywhere without changing f₀ near K. The assumpt...
Source project: Sphere eversion
Person-level attribution pending.
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.