Commit 2023-06-05 01:20 e3fdf992

View on Github →

refactor: add abbreviations with explicit arguments (#4641) Lean 4 does not support [] fields in classes, so some definitions like ChartedSpace.atlas have fewer explicit arguments than they used to have in Lean 3. This PR adds abbreviations in the root namespace with explicit arguments.

Estimated changes

modified def achart
modified theorem achart_def
modified theorem achart_val
added theorem chart_mem_atlas
modified theorem chart_source_mem_nhds
modified theorem chart_target_mem_nhds
modified theorem coe_achart
added theorem mem_chart_source
modified theorem mem_chart_target