Commit 2023-06-23 23:13 08077c33

View on Github →

feat: supporting lemmas for port of ContMDiff (#5428) Instead of fixing a proof "as is", I'm golfing it and moving parts of it to lemmas.

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiffDef.lean

added theorem contDiffWithinAt_insert_self

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

added theorem ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range

added theorem LocalHomeomorph.continuousOn_writtenInExtend_iff

added theorem LocalHomeomorph.continuousWithinAt_writtenInExtend_iff

added theorem LocalHomeomorph.map_extend_nhdsWithin_eq_image_of_subset

added theorem LocalHomeomorph.tendsto_extend_comp_iff

Modified Mathlib/Topology/ContinuousOn.lean

added theorem continuousWithinAt_congr_nhds