feat(geometry/manifold/smooth_manifold_with_corners): define local_ho…

…meomorph.extend (#17669)

* This generalizes the API of `ext_chart_at` to arbitrary local homeomorphisms
* This allows us to generalize a bunch of properties of `ext_chart_at` (like smoothness) to arbitrary members of the atlas.
* Fix some names: (primed versions are similarly renamed)
```
ext_chart_at_open_source -> is_open_ext_chart_at_source
nhds_within_ext_chart_target_eq -> nhds_within_ext_chart_at_target_eq
ext_chart_continuous_at_symm -> ext_chart_at_continuous_at_symm
ext_chart_continuous_on_symm -> ext_chart_at_continuous_on_symm
ext_chart_self_eq -> ext_chart_at_self_eq
ext_chart_self_apply -> ext_chart_at_self_apply
ext_chart_at_continuous_on -> continuous_on_ext_chart_at
ext_chart_at_continuous_at -> continuous_at_ext_chart_at
ext_chart_preimage_open_of_open -> is_open_ext_chart_at_preimage
ext_chart_at_map_* -> map_ext_chart_at_*
ext_chart_at_symm_map_* -> map_ext_chart_at_symm_*
ext_chart_preimage_mem_nhds_within -> ext_chart_at_preimage_mem_nhds_within
ext_chart_preimage_mem_nhds -> ext_chart_at_preimage_mem_nhds
ext_chart_preimage_inter_eq -> ext_chart_at_preimage_inter_eq
ext_chart_model_space_eq_id -> ext_chart_at_model_space_eq_id
ext_chart_model_space_apply -> ext_chart_at_model_space_apply
```
* One notable unchanged (wrong) name is `mem_ext_chart_source`, but that should be renamed together with `mem_chart_source`.
* Motivated by the sphere eversion project

src/geometry/manifold/bump_function.lean

@@ -105,7 +105,7 @@ by rw [coe_def, support_indicator, (∘), support_comp_eq_preimage, ← ext_char
   ← (ext_chart_at I c).symm_image_target_inter_eq', f.to_cont_diff_bump.support_eq]
 
 lemma is_open_support : is_open (support f) :=
-by { rw support_eq_inter_preimage, exact ext_chart_preimage_open_of_open I c is_open_ball }
+by { rw support_eq_inter_preimage, exact is_open_ext_chart_at_preimage I c is_open_ball }
 
 lemma support_eq_symm_image :
   support f = (ext_chart_at I c).symm '' (ball (ext_chart_at I c c) f.R ∩ range I) :=
@@ -152,7 +152,7 @@ lemma eventually_eq_one_of_dist_lt (hs : x ∈ (chart_at H c).source)
   (hd : eudist (ext_chart_at I c x) (ext_chart_at I c c) < f.r) :
   f =ᶠ[𝓝 x] 1 :=
 begin
-  filter_upwards [is_open.mem_nhds (ext_chart_preimage_open_of_open I c is_open_ball) ⟨hs, hd⟩],
+  filter_upwards [is_open.mem_nhds (is_open_ext_chart_at_preimage I c is_open_ball) ⟨hs, hd⟩],
   rintro z ⟨hzs, hzd : _ < _⟩,
   exact f.one_of_dist_le hzs hzd.le
 end
@@ -176,7 +176,7 @@ lemma nonempty_support : (support f).nonempty := ⟨c, f.c_mem_support⟩
 lemma compact_symm_image_closed_ball :
   is_compact ((ext_chart_at I c).symm '' (closed_ball (ext_chart_at I c c) f.R ∩ range I)) :=
 (euclidean.is_compact_closed_ball.inter_right I.closed_range).image_of_continuous_on $
-  (ext_chart_at_continuous_on_symm _ _).mono f.closed_ball_subset
+  (continuous_on_ext_chart_at_symm _ _).mono f.closed_ball_subset
 
 /-- Given a smooth bump function `f : smooth_bump_function I c`, the closed ball of radius `f.R` is
 known to include the support of `f`. These closed balls (in the model normed space `E`) intersected
@@ -198,7 +198,7 @@ lemma is_closed_image_of_is_closed {s : set M} (hsc : is_closed s) (hs : s ⊆ s
 begin
   rw f.image_eq_inter_preimage_of_subset_support hs,
   refine continuous_on.preimage_closed_of_closed
-    ((ext_chart_continuous_on_symm _ _).mono f.closed_ball_subset) _ hsc,
+    ((continuous_on_ext_chart_at_symm _ _).mono f.closed_ball_subset) _ hsc,
   exact is_closed.inter is_closed_closed_ball I.closed_range
 end
 
@@ -273,7 +273,7 @@ lemma nhds_basis_tsupport :
 begin
   have : (𝓝 c).has_basis (λ f : smooth_bump_function I c, true)
     (λ f, (ext_chart_at I c).symm '' (closed_ball (ext_chart_at I c c) f.R ∩ range I)),
-  { rw [← ext_chart_at_symm_map_nhds_within_range I c],
+  { rw [← map_ext_chart_at_symm_nhds_within_range I c],
     exact nhds_within_range_basis.map _ },
   refine this.to_has_basis' (λ f hf, ⟨f, trivial, f.tsupport_subset_symm_image_closed_ball⟩)
     (λ f _, f.tsupport_mem_nhds),

src/geometry/manifold/cont_mdiff.lean

@@ -286,8 +286,8 @@ begin
   rw [cont_mdiff_within_at_iff, and.congr_right_iff],
   set e := ext_chart_at I x, set e' := ext_chart_at I' (f x),
   refine λ hc, cont_diff_within_at_congr_nhds _,
-  rw [← e.image_source_inter_eq', ← ext_chart_at_map_nhds_within_eq_image,
-      ← ext_chart_at_map_nhds_within, inter_comm, nhds_within_inter_of_mem],
+  rw [← e.image_source_inter_eq', ← map_ext_chart_at_nhds_within_eq_image,
+      ← map_ext_chart_at_nhds_within, inter_comm, nhds_within_inter_of_mem],
   exact hc (ext_chart_at_source_mem_nhds _ _)
 end
 
@@ -306,9 +306,9 @@ begin
     refine ((I'.continuous_at.comp_continuous_within_at h₂).comp' h).mono_of_mem _,
     exact inter_mem self_mem_nhds_within (h.preimage_mem_nhds_within $
       (chart_at _ _).open_source.mem_nhds $ mem_chart_source _ _) },
-  simp_rw [cont, cont_diff_within_at_prop, ext_chart_at, local_equiv.coe_trans,
-    model_with_corners.to_local_equiv_coe, local_homeomorph.coe_coe, model_with_corners_self_coe,
-    chart_at_self_eq, local_homeomorph.refl_apply, comp.left_id]
+  simp_rw [cont, cont_diff_within_at_prop, ext_chart_at, local_homeomorph.extend,
+    local_equiv.coe_trans, model_with_corners.to_local_equiv_coe, local_homeomorph.coe_coe,
+    model_with_corners_self_coe, chart_at_self_eq, local_homeomorph.refl_apply, comp.left_id]
 end
 
 lemma smooth_within_at_iff :
@@ -359,9 +359,9 @@ begin
   rw [and.congr_right_iff],
   set e := ext_chart_at I x, set e' := ext_chart_at I' (f x),
   refine λ hc, cont_diff_within_at_congr_nhds _,
-  rw [← e.image_source_inter_eq', ← ext_chart_at_map_nhds_within_eq_image' I x hx,
-      ← ext_chart_at_map_nhds_within' I x hx, inter_comm, nhds_within_inter_of_mem],
-  exact hc ((ext_chart_at_open_source _ _).mem_nhds hy)
+  rw [← e.image_source_inter_eq', ← map_ext_chart_at_nhds_within_eq_image' I x hx,
+      ← map_ext_chart_at_nhds_within' I x hx, inter_comm, nhds_within_inter_of_mem],
+  exact hc (ext_chart_at_source_mem_nhds' _ _ hy)
 end
 
 lemma cont_mdiff_at_iff_of_mem_source {x' : M} {y : M'} (hx : x' ∈ (chart_at H x).source)
@@ -387,7 +387,7 @@ begin
   simp_rw [structure_groupoid.lift_prop_within_at_self_target],
   simp_rw [((chart_at H' y).continuous_at hy).comp_continuous_within_at hf],
   rw [← ext_chart_at_source I'] at hy,
-  simp_rw [(ext_chart_at_continuous_at' I' _ hy).comp_continuous_within_at hf],
+  simp_rw [(continuous_at_ext_chart_at' I' _ hy).comp_continuous_within_at hf],
   refl,
 end
 
@@ -453,7 +453,7 @@ lemma cont_mdiff_at_ext_chart_at' {x' : M} (h : x' ∈ (chart_at H x).source) :
 begin
   refine (cont_mdiff_at_iff_of_mem_source h (mem_chart_source _ _)).mpr _,
   rw [← ext_chart_at_source I] at h,
-  refine ⟨ext_chart_at_continuous_at' _ _ h, _⟩,
+  refine ⟨continuous_at_ext_chart_at' _ _ h, _⟩,
   refine cont_diff_within_at_id.congr_of_eventually_eq _ _,
   { refine eventually_eq_of_mem (ext_chart_at_target_mem_nhds_within' I x h) (λ x₂ hx₂, _),
     simp_rw [function.comp_apply, (ext_chart_at I x).right_inv hx₂], refl },
@@ -490,7 +490,7 @@ begin
     refine (h2 _ $ mem_image_of_mem _ hx').mono_of_mem _,
     rw [← ext_chart_at_source I] at hs,
     rw [(ext_chart_at I x).image_eq_target_inter_inv_preimage hs],
-    refine inter_mem _ (ext_chart_preimage_mem_nhds_within' I x (hs hx') self_mem_nhds_within),
+    refine inter_mem _ (ext_chart_at_preimage_mem_nhds_within' I x (hs hx') self_mem_nhds_within),
     have := ext_chart_at_target_mem_nhds_within' I x (hs hx'),
     refine nhds_within_mono _ (inter_subset_right _ _) this }
 end
@@ -532,8 +532,8 @@ lemma cont_mdiff_on_iff_target :
 begin
   inhabit E',
   simp only [cont_mdiff_on_iff, model_with_corners.source_eq, chart_at_self_eq,
-    local_homeomorph.refl_local_equiv, local_equiv.refl_trans, ext_chart_at.equations._eqn_1,
-    set.preimage_univ, set.inter_univ, and.congr_right_iff],
+    local_homeomorph.refl_local_equiv, local_equiv.refl_trans, ext_chart_at,
+    local_homeomorph.extend, set.preimage_univ, set.inter_univ, and.congr_right_iff],
   intros h,
   split,
   { refine λ h' y, ⟨_, λ x _, h' x y⟩,
@@ -768,7 +768,7 @@ begin
     { rw nhds_within_restrict _ xo o_open,
       refine filter.inter_mem self_mem_nhds_within _,
       suffices : u ∈ 𝓝[(ext_chart_at I x) '' (insert x s ∩ o)] (ext_chart_at I x x),
-        from (ext_chart_at_continuous_at I x).continuous_within_at.preimage_mem_nhds_within' this,
+        from (continuous_at_ext_chart_at I x).continuous_within_at.preimage_mem_nhds_within' this,
       apply nhds_within_mono _ _ u_nhds,
       rw image_subset_iff,
       assume y hy,
@@ -778,8 +778,8 @@ begin
     show cont_mdiff_on I I' n f v,
     { assume y hy,
       have : continuous_within_at f v y,
-      { apply (((ext_chart_at_continuous_on_symm I' (f x) _ _).comp'
-          (hu _ hy.2).continuous_within_at).comp' (ext_chart_at_continuous_on I x _ _)).congr_mono,
+      { apply (((continuous_on_ext_chart_at_symm I' (f x) _ _).comp'
+          (hu _ hy.2).continuous_within_at).comp' (continuous_on_ext_chart_at I x _ _)).congr_mono,
         { assume z hz,
           simp only [v_incl hz, v_incl' z hz] with mfld_simps },
         { assume z hz,
@@ -898,7 +898,7 @@ begin
   rw this at hg,
   have A : ∀ᶠ y in 𝓝[e.symm ⁻¹' s ∩ range I] e x,
     y ∈ e.target ∧ f (e.symm y) ∈ t ∧ f (e.symm y) ∈ e'.source ∧ g (f (e.symm y)) ∈ e''.source,
-  { simp only [← ext_chart_at_map_nhds_within, eventually_map],
+  { simp only [← map_ext_chart_at_nhds_within, eventually_map],
     filter_upwards [hf.1.tendsto (ext_chart_at_source_mem_nhds I' (f x)),
       (hg.1.comp hf.1 st).tendsto (ext_chart_at_source_mem_nhds I'' (g (f x))),
       (inter_mem_nhds_within s (ext_chart_at_source_mem_nhds I x))],
@@ -1535,7 +1535,7 @@ lemma cont_mdiff_within_at_pi_space :
     ∀ i, cont_mdiff_within_at I (𝓘(𝕜, Fi i)) n (λ x, φ x i) s x :=
 by simp only [cont_mdiff_within_at_iff, continuous_within_at_pi,
   cont_diff_within_at_pi, forall_and_distrib, written_in_ext_chart_at,
-  ext_chart_model_space_eq_id, (∘), local_equiv.refl_coe, id]
+  ext_chart_at_model_space_eq_id, (∘), local_equiv.refl_coe, id]
 
 lemma cont_mdiff_on_pi_space :
   cont_mdiff_on I (𝓘(𝕜, Π i, Fi i)) n φ s ↔

src/geometry/manifold/cont_mdiff_mfderiv.lean

@@ -54,7 +54,7 @@ begin
   suffices h : mdifferentiable_within_at I I' f (s ∩ (f ⁻¹' (ext_chart_at I' (f x)).source)) x,
   { rwa mdifferentiable_within_at_inter' at h,
     apply (hf.1).preimage_mem_nhds_within,
-    exact is_open.mem_nhds (ext_chart_at_open_source I' (f x)) (mem_ext_chart_source I' (f x)) },
+    exact ext_chart_at_source_mem_nhds I' (f x) },
   rw mdifferentiable_within_at_iff,
   exact ⟨hf.1.mono (inter_subset_left _ _),
     (hf.2.differentiable_within_at hn).mono (by mfld_set_tac)⟩,

src/geometry/manifold/mfderiv.lean

@@ -337,7 +337,7 @@ lemma unique_mdiff_within_at_iff {s : set M} {x : M} :
   ((ext_chart_at I x) x) :=
 begin
   apply unique_diff_within_at_congr,
-  rw [nhds_within_inter, nhds_within_inter, nhds_within_ext_chart_target_eq]
+  rw [nhds_within_inter, nhds_within_inter, nhds_within_ext_chart_at_target_eq]
 end
 
 lemma unique_mdiff_within_at.mono (h : unique_mdiff_within_at I s x) (st : s ⊆ t) :
@@ -347,15 +347,15 @@ unique_diff_within_at.mono h $ inter_subset_inter (preimage_mono st) (subset.ref
 lemma unique_mdiff_within_at.inter' (hs : unique_mdiff_within_at I s x) (ht : t ∈ 𝓝[s] x) :
   unique_mdiff_within_at I (s ∩ t) x :=
 begin
-  rw [unique_mdiff_within_at, ext_chart_preimage_inter_eq],
-  exact unique_diff_within_at.inter' hs (ext_chart_preimage_mem_nhds_within I x ht)
+  rw [unique_mdiff_within_at, ext_chart_at_preimage_inter_eq],
+  exact unique_diff_within_at.inter' hs (ext_chart_at_preimage_mem_nhds_within I x ht)
 end
 
 lemma unique_mdiff_within_at.inter (hs : unique_mdiff_within_at I s x) (ht : t ∈ 𝓝 x) :
   unique_mdiff_within_at I (s ∩ t) x :=
 begin
-  rw [unique_mdiff_within_at, ext_chart_preimage_inter_eq],
-  exact unique_diff_within_at.inter hs (ext_chart_preimage_mem_nhds I x ht)
+  rw [unique_mdiff_within_at, ext_chart_at_preimage_inter_eq],
+  exact unique_diff_within_at.inter hs (ext_chart_at_preimage_mem_nhds I x ht)
 end
 
 lemma is_open.unique_mdiff_within_at (xs : x ∈ s) (hs : is_open s) : unique_mdiff_within_at I s x :=
@@ -408,7 +408,7 @@ lemma mdifferentiable_within_at_iff {f : M → M'} {s : set M} {x : M} :
 begin
   refine and_congr iff.rfl (exists_congr $ λ f', _),
   rw [inter_comm],
-  simp only [has_fderiv_within_at, nhds_within_inter, nhds_within_ext_chart_target_eq]
+  simp only [has_fderiv_within_at, nhds_within_inter, nhds_within_ext_chart_at_target_eq]
 end
 
 include Is I's
@@ -468,17 +468,17 @@ end
 lemma has_mfderiv_within_at_inter' (h : t ∈ 𝓝[s] x) :
   has_mfderiv_within_at I I' f (s ∩ t) x f' ↔ has_mfderiv_within_at I I' f s x f' :=
 begin
-  rw [has_mfderiv_within_at, has_mfderiv_within_at, ext_chart_preimage_inter_eq,
+  rw [has_mfderiv_within_at, has_mfderiv_within_at, ext_chart_at_preimage_inter_eq,
       has_fderiv_within_at_inter', continuous_within_at_inter' h],
-  exact ext_chart_preimage_mem_nhds_within I x h,
+  exact ext_chart_at_preimage_mem_nhds_within I x h,
 end
 
 lemma has_mfderiv_within_at_inter (h : t ∈ 𝓝 x) :
   has_mfderiv_within_at I I' f (s ∩ t) x f' ↔ has_mfderiv_within_at I I' f s x f' :=
 begin
-  rw [has_mfderiv_within_at, has_mfderiv_within_at, ext_chart_preimage_inter_eq,
+  rw [has_mfderiv_within_at, has_mfderiv_within_at, ext_chart_at_preimage_inter_eq,
       has_fderiv_within_at_inter, continuous_within_at_inter h],
-  exact ext_chart_preimage_mem_nhds I x h,
+  exact ext_chart_at_preimage_mem_nhds I x h,
 end
 
 lemma has_mfderiv_within_at.union
@@ -564,17 +564,17 @@ by simp only [mdifferentiable_within_at, mdifferentiable_at, continuous_within_a
 lemma mdifferentiable_within_at_inter (ht : t ∈ 𝓝 x) :
   mdifferentiable_within_at I I' f (s ∩ t) x ↔ mdifferentiable_within_at I I' f s x :=
 begin
-  rw [mdifferentiable_within_at, mdifferentiable_within_at, ext_chart_preimage_inter_eq,
+  rw [mdifferentiable_within_at, mdifferentiable_within_at, ext_chart_at_preimage_inter_eq,
       differentiable_within_at_inter, continuous_within_at_inter ht],
-  exact ext_chart_preimage_mem_nhds I x ht
+  exact ext_chart_at_preimage_mem_nhds I x ht
 end
 
 lemma mdifferentiable_within_at_inter' (ht : t ∈ 𝓝[s] x) :
   mdifferentiable_within_at I I' f (s ∩ t) x ↔ mdifferentiable_within_at I I' f s x :=
 begin
-  rw [mdifferentiable_within_at, mdifferentiable_within_at, ext_chart_preimage_inter_eq,
+  rw [mdifferentiable_within_at, mdifferentiable_within_at, ext_chart_at_preimage_inter_eq,
       differentiable_within_at_inter', continuous_within_at_inter' ht],
-  exact ext_chart_preimage_mem_nhds_within I x ht
+  exact ext_chart_at_preimage_mem_nhds_within I x ht
 end
 
 lemma mdifferentiable_at.mdifferentiable_within_at
@@ -619,8 +619,9 @@ end
 
 lemma mfderiv_within_inter (ht : t ∈ 𝓝 x) (hs : unique_mdiff_within_at I s x) :
   mfderiv_within I I' f (s ∩ t) x = mfderiv_within I I' f s x :=
-by rw [mfderiv_within, mfderiv_within, ext_chart_preimage_inter_eq,
-  mdifferentiable_within_at_inter ht, fderiv_within_inter (ext_chart_preimage_mem_nhds I x ht) hs]
+by rw [mfderiv_within, mfderiv_within, ext_chart_at_preimage_inter_eq,
+  mdifferentiable_within_at_inter ht,
+  fderiv_within_inter (ext_chart_at_preimage_mem_nhds I x ht) hs]
 
 lemma mdifferentiable_at_iff_of_mem_source {x' : M} {y : M'}
   (hx : x' ∈ (charted_space.chart_at H x).source)
@@ -705,7 +706,7 @@ begin
   apply has_fderiv_within_at.congr_of_eventually_eq h.2,
   { have : (ext_chart_at I x).symm ⁻¹' {y | f₁ y = f y} ∈
       𝓝[(ext_chart_at I x).symm ⁻¹' s ∩ range I] ((ext_chart_at I x) x)  :=
-      ext_chart_preimage_mem_nhds_within I x h₁,
+      ext_chart_at_preimage_mem_nhds_within I x h₁,
     apply filter.mem_of_superset this (λy, _),
     simp only [hx] with mfld_simps {contextual := tt} },
   { simp only [hx] with mfld_simps },
@@ -816,7 +817,7 @@ lemma written_in_ext_chart_comp (h : continuous_within_at f s x) :
 begin
   apply @filter.mem_of_superset _ _
     ((f ∘ (ext_chart_at I x).symm)⁻¹' (ext_chart_at I' (f x)).source) _
-    (ext_chart_preimage_mem_nhds_within I x
+    (ext_chart_at_preimage_mem_nhds_within I x
       (h.preimage_mem_nhds_within (ext_chart_at_source_mem_nhds _ _))),
   mfld_set_tac,
 end
@@ -837,10 +838,10 @@ begin
     ((ext_chart_at I x) x),
   { have : (ext_chart_at I x).symm ⁻¹' (f ⁻¹' (ext_chart_at I' (f x)).source)
     ∈ 𝓝[(ext_chart_at I x).symm ⁻¹' s ∩ range I] ((ext_chart_at I x) x)  :=
-      (ext_chart_preimage_mem_nhds_within I x
+      (ext_chart_at_preimage_mem_nhds_within I x
         (hf.1.preimage_mem_nhds_within (ext_chart_at_source_mem_nhds _ _))),
     unfold has_mfderiv_within_at at *,
-    rw [← has_fderiv_within_at_inter' this, ← ext_chart_preimage_inter_eq] at hf ⊢,
+    rw [← has_fderiv_within_at_inter' this, ← ext_chart_at_preimage_inter_eq] at hf ⊢,
     have : written_in_ext_chart_at I I' x f ((ext_chart_at I x) x)
         = (ext_chart_at I' (f x)) (f x),
       by simp only with mfld_simps,
@@ -1609,7 +1610,7 @@ begin
   { have : unique_mdiff_within_at I s z := hs _ hx.2,
     have S : e.source ∩ e ⁻¹' ((ext_chart_at I' x).source) ∈ 𝓝 z,
     { apply is_open.mem_nhds,
-      apply e.continuous_on.preimage_open_of_open e.open_source (ext_chart_at_open_source I' x),
+      apply e.continuous_on.preimage_open_of_open e.open_source (is_open_ext_chart_at_source I' x),
       simp only [z_source, zx] with mfld_simps },
     have := this.inter S,
     rw [unique_mdiff_within_at_iff] at this,
@@ -1685,7 +1686,7 @@ begin
   { assume z hz,
     apply (hs z hz.1).inter',
     apply (hf z hz.1).preimage_mem_nhds_within,
-    exact is_open.mem_nhds (ext_chart_at_open_source I' y) hz.2 },
+    exact (is_open_ext_chart_at_source I' y).mem_nhds hz.2 },
   exact this.unique_diff_on_target_inter _
 end