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 3 research declarations. Search 10,000 more complete Mathlib declarations.
3 results
Clear filtersoneJetBundle_chart_source
Plain-language statement
In J¹(M, M'), the source of a chart has a nice formula
Source project: Sphere eversion
Person-level attribution pending.
oneJetBundle_chart_target
Plain-language statement
In J¹(M, M'), the target of a chart has a nice formula
Source project: Sphere eversion
Person-level attribution pending.
oneJetBundle_model_space_chartAt
Plain-language statement
In the OneJetBundle to the model space, the charts are just the canonical identification between a product type and a bundle total space type, a.k.a. Bundle.TotalSpace.toProd.
Source project: Sphere eversion
Person-level attribution pending.