Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-06 11:16 f09322bc

View on Github →

feat(geometry/manifold/local_invariant_properties): simplify definitions and proofs (#15116)

  • Simplify the sets in local_invariant_prop and lift_prop_within_at
  • Simplify many proofs in local_invariant_properties.lean
  • Reorder the intersection in cont_diff_within_at_prop to be more consistent with all lemmas in smooth_manifold_with_corners.lean
  • New lemmas, such as cont_mdiff_within_at_iff_of_mem_source and properties of local_invariant_prop
  • I expect that some lemmas in cont_mdiff.lean can be simplified using the new definitions, but I don't do that in this PR.
  • Lemma renamings:
cont_mdiff_within_at_iff -> cont_mdiff_within_at_iff'
cont_mdiff_within_at_iff' -> cont_mdiff_within_at_iff_of_mem_source'
cont_mdiff_within_at_iff'' -> cont_mdiff_within_at_iff [or iff.rfl]

Estimated changes

added theorem chart_source_mem_nhds
added theorem chart_target_mem_nhds
modified theorem cont_mdiff_at_ext_chart_at
added theorem cont_mdiff_at_iff
modified theorem cont_mdiff_within_at_iff'