Commit 2024-02-01 10:54 a2c91ca1

View on Github →

refactor(PartialHomeomorph): Remove explicit variable (x : M). (#10083) Instead, supply it as needed. This replaces an explicit argument (x : M) by an implicit {x : M} in the following lemmas:

extChartAt_source_mem_nhds'
extChartAt_source_mem_nhdsWithin'
continuousAt_extChartAt'
extChartAt_image_nhd_mem_nhds_of_boundaryless
extChartAt_target_mem_nhdsWithin'
nhdsWithin_extChartAt_target_eq'
continuousAt_extChartAt_symm'
continuousAt_extChartAt_symm''
map_extChartAt_nhdsWithin_eq_image'
map_extChartAt_nhdsWithin'
map_extChartAt_symm_nhdsWithin'
map_extChartAt_symm_nhdsWithin_range'
extChartAt_preimage_mem_nhdsWithin'
extChartAt_preimage_mem_nhdsWithin
extChartAt_preimage_mem_nhds'
extChartAt_preimage_mem_nhds

Estimated changes

Modified Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

Modified Mathlib/Geometry/Manifold/IntegralCurve.lean

Modified Mathlib/Geometry/Manifold/MFDeriv/Basic.lean

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

modified theorem continuousAt_extChartAt'

modified theorem continuousAt_extChartAt

modified theorem continuousAt_extChartAt_symm''

modified theorem continuousAt_extChartAt_symm'

modified theorem continuousAt_extChartAt_symm

modified theorem continuousOn_extChartAt

modified theorem continuousOn_extChartAt_symm

modified theorem extChartAt_coe

modified theorem extChartAt_coe_symm

modified theorem extChartAt_preimage_inter_eq

modified theorem extChartAt_preimage_mem_nhds'

modified theorem extChartAt_preimage_mem_nhds

modified theorem extChartAt_preimage_mem_nhdsWithin'

modified theorem extChartAt_preimage_mem_nhdsWithin

modified theorem extChartAt_source

modified theorem extChartAt_source_mem_nhds'

modified theorem extChartAt_source_mem_nhds

modified theorem extChartAt_source_mem_nhdsWithin'

modified theorem extChartAt_source_mem_nhdsWithin

modified theorem extChartAt_target_mem_nhdsWithin'

modified theorem extChartAt_target_mem_nhdsWithin

modified theorem extChartAt_target_subset_range

modified theorem extChartAt_to_inv

modified theorem isOpen_extChartAt_preimage'

modified theorem isOpen_extChartAt_preimage

modified theorem isOpen_extChartAt_source

modified theorem map_extChartAt_nhds

modified theorem map_extChartAt_nhdsWithin'

modified theorem map_extChartAt_nhdsWithin

modified theorem map_extChartAt_nhdsWithin_eq_image'

modified theorem map_extChartAt_nhdsWithin_eq_image

modified theorem map_extChartAt_nhds_of_boundaryless

modified theorem map_extChartAt_symm_nhdsWithin'

modified theorem map_extChartAt_symm_nhdsWithin

modified theorem map_extChartAt_symm_nhdsWithin_range'

modified theorem map_extChartAt_symm_nhdsWithin_range

modified theorem mapsTo_extChartAt

modified theorem mem_extChartAt_source

modified theorem mem_extChartAt_target

modified theorem nhdsWithin_extChartAt_target_eq'

modified theorem nhdsWithin_extChartAt_target_eq