chore(geometry/manifold): use namespace, rename image to `image_e…

…q` (#6517)

* use `namespace` command in
  `geometry/manifold/smooth_manifold_with_corners`;
* rename `model_with_corners.image` to `model_with_corners.image_eq`
  to match `source_eq` etc;
* replace `homeomorph.coe_eq_to_equiv` with
  `@[simp] lemma coe_to_equiv`;
* add `continuous_linear_map.symm_image_image` and
  `continuous_linear_map.image_symm_image`;
* add `unique_diff_on.image`,
  `continuous_linear_equiv.unique_diff_on_image_iff`.

src/analysis/calculus/fderiv.lean

@@ -2766,32 +2766,28 @@ begin
   exact h.maps_to_tangent_cone.mono (subset.refl _) submodule.subset_span
 end
 
+lemma unique_diff_on.image {f' : E → E →L[𝕜] F} (hs : unique_diff_on 𝕜 s)
+  (hf' : ∀ x ∈ s, has_fderiv_within_at f (f' x) s x) (hd : ∀ x ∈ s, dense_range (f' x)) :
+  unique_diff_on 𝕜 (f '' s) :=
+ball_image_iff.2 $ λ x hx, (hf' x hx).unique_diff_within_at (hs x hx) (hd x hx)
+
 lemma has_fderiv_within_at.unique_diff_within_at_of_continuous_linear_equiv
   {x : E} (e' : E ≃L[𝕜] F) (h : has_fderiv_within_at f (e' : E →L[𝕜] F) s x)
   (hs : unique_diff_within_at 𝕜 s x) :
   unique_diff_within_at 𝕜 (f '' s) (f x) :=
 h.unique_diff_within_at hs e'.surjective.dense_range
 
-lemma continuous_linear_equiv.unique_diff_on_preimage_iff (e : F ≃L[𝕜] E) :
+lemma continuous_linear_equiv.unique_diff_on_image (e : E ≃L[𝕜] F) (h : unique_diff_on 𝕜 s) :
+  unique_diff_on 𝕜 (e '' s) :=
+h.image (λ x _, e.has_fderiv_within_at) (λ x hx, e.surjective.dense_range)
+
+@[simp] lemma continuous_linear_equiv.unique_diff_on_image_iff (e : E ≃L[𝕜] F) :
+  unique_diff_on 𝕜 (e '' s) ↔ unique_diff_on 𝕜 s :=
+⟨λ h, e.symm_image_image s ▸ e.symm.unique_diff_on_image h, e.unique_diff_on_image⟩
+
+@[simp] lemma continuous_linear_equiv.unique_diff_on_preimage_iff (e : F ≃L[𝕜] E) :
   unique_diff_on 𝕜 (e ⁻¹' s) ↔ unique_diff_on 𝕜 s :=
-begin
-  split,
-  { assume hs x hx,
-    have A : s = e '' (e.symm '' s) :=
-      (equiv.symm_image_image (e.symm.to_linear_equiv.to_equiv) s).symm,
-    have B : e.symm '' s = e⁻¹' s :=
-      equiv.image_eq_preimage e.symm.to_linear_equiv.to_equiv s,
-    rw [A, B, (e.apply_symm_apply x).symm],
-    refine has_fderiv_within_at.unique_diff_within_at_of_continuous_linear_equiv e
-      e.has_fderiv_within_at (hs _ _),
-    rwa [mem_preimage, e.apply_symm_apply x] },
-  { assume hs x hx,
-    have : e ⁻¹' s = e.symm '' s :=
-      (equiv.image_eq_preimage e.symm.to_linear_equiv.to_equiv s).symm,
-    rw [this, (e.symm_apply_apply x).symm],
-    exact has_fderiv_within_at.unique_diff_within_at_of_continuous_linear_equiv e.symm
-      e.symm.has_fderiv_within_at (hs _ hx) },
-end
+by rw [← e.image_symm_eq_preimage, e.symm.unique_diff_on_image_iff]
 
 end tangent_cone
 

src/geometry/manifold/basic_smooth_bundle.lean

@@ -261,7 +261,7 @@ begin
       cocycle property one can get rid of it, and then conclude using the smoothness of the
       cocycle as given in the definition of basic smooth bundles. -/
       have := Z.coord_change_smooth ⟨e, he⟩ ⟨e', he'⟩,
-      rw model_with_corners.image at this,
+      rw I.image_eq at this,
       apply times_cont_diff_on.congr this,
       rintros ⟨x, v⟩ hx,
       simp only with mfld_simps at hx,
@@ -297,7 +297,7 @@ def tangent_bundle_core : basic_smooth_bundle_core I M E :=
   coord_change_smooth := λi j, begin
     /- To check that the coordinate change of the bundle is smooth, one should just use the
     smoothness of the charts, and thus the smoothness of their derivatives. -/
-    rw model_with_corners.image,
+    rw I.image_eq,
     have A : times_cont_diff_on 𝕜 ∞
       (I ∘ (i.1.symm.trans j.1) ∘ I.symm)
       (I.symm ⁻¹' (i.1.symm.trans j.1).source ∩ range I) :=
@@ -343,9 +343,9 @@ def tangent_bundle_core : basic_smooth_bundle_core I M E :=
       simp only [hx, i.1.map_target] with mfld_simps },
     have B : ∀ᶠ y in 𝓝[range I] (I x),
       (I ∘ i.1 ∘ i.1.symm ∘ I.symm) y = (id : E → E) y,
-    { apply filter.mem_sets_of_superset A,
+    { filter_upwards [A],
       assume y hy,
-      rw ← model_with_corners.image at hy,
+      rw ← I.image_eq at hy,
       rcases hy with ⟨z, hz⟩,
       simp only with mfld_simps at hz,
       simp only [hz.2.symm, hz.1] with mfld_simps },

src/geometry/manifold/smooth_manifold_with_corners.lean

@@ -161,101 +161,85 @@ variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
   {E : Type*} [normed_group E] [normed_space 𝕜 E] {H : Type*} [topological_space H]
   (I : model_with_corners 𝕜 E H)
 
+namespace model_with_corners
+
 instance : has_coe_to_fun (model_with_corners 𝕜 E H) := ⟨_, λ e, e.to_fun⟩
 
 /-- The inverse to a model with corners, only registered as a local equiv. -/
-protected def model_with_corners.symm : local_equiv E H := I.to_local_equiv.symm
+protected def symm : local_equiv E H := I.to_local_equiv.symm
 
 /- Register a few lemmas to make sure that `simp` puts expressions in normal form -/
-@[simp, mfld_simps] lemma model_with_corners.to_local_equiv_coe : (I.to_local_equiv : H → E) = I :=
+@[simp, mfld_simps] lemma to_local_equiv_coe : (I.to_local_equiv : H → E) = I :=
 rfl
 
-@[simp, mfld_simps] lemma model_with_corners.mk_coe (e : local_equiv H E) (a b c d) :
+@[simp, mfld_simps] lemma mk_coe (e : local_equiv H E) (a b c d) :
   ((model_with_corners.mk e a b c d : model_with_corners 𝕜 E H) : H → E) = (e : H → E) := rfl
 
-@[simp, mfld_simps] lemma model_with_corners.to_local_equiv_coe_symm :
-  (I.to_local_equiv.symm : E → H) = I.symm := rfl
+@[simp, mfld_simps] lemma to_local_equiv_coe_symm : (I.to_local_equiv.symm : E → H) = I.symm := rfl
 
-@[simp, mfld_simps] lemma model_with_corners.mk_coe_symm (e : local_equiv H E) (a b c d) :
-  ((model_with_corners.mk e a b c d : model_with_corners 𝕜 E H).symm : E → H) = (e.symm : E → H) :=
+@[simp, mfld_simps] lemma mk_symm (e : local_equiv H E) (a b c d) :
+  (model_with_corners.mk e a b c d : model_with_corners 𝕜 E H).symm = e.symm :=
 rfl
 
-lemma model_with_corners.unique_diff : unique_diff_on 𝕜 (range I) := I.unique_diff'
+protected lemma unique_diff : unique_diff_on 𝕜 (range I) := I.unique_diff'
 
-protected lemma model_with_corners.continuous : continuous I := I.continuous_to_fun
+@[continuity] protected lemma continuous : continuous I := I.continuous_to_fun
 
-lemma model_with_corners.continuous_symm : continuous I.symm := I.continuous_inv_fun
+@[continuity] lemma continuous_symm : continuous I.symm := I.continuous_inv_fun
 
-section
-variables (𝕜 E)
-
-/-- In the trivial model with corners, the associated local equiv is the identity. -/
-@[simp, mfld_simps] lemma model_with_corners_self_local_equiv :
-  (model_with_corners_self 𝕜 E).to_local_equiv = local_equiv.refl E := rfl
-
-@[simp, mfld_simps] lemma model_with_corners_self_coe :
-  (model_with_corners_self 𝕜 E : E → E) = id := rfl
-
-@[simp, mfld_simps] lemma model_with_corners_self_coe_symm :
-  ((model_with_corners_self 𝕜 E).symm : E → E) = id := rfl
-
-end
-
-@[simp, mfld_simps] lemma model_with_corners.target_eq : I.target = range (I : H → E) :=
+@[simp, mfld_simps] lemma target_eq : I.target = range (I : H → E) :=
 by { rw [← image_univ, ← I.source_eq], exact (I.to_local_equiv.image_source_eq_target).symm }
 
-@[simp, mfld_simps] lemma model_with_corners.left_inv (x : H) : I.symm (I x) = x :=
+@[simp, mfld_simps] protected lemma left_inv (x : H) : I.symm (I x) = x :=
 by { refine I.left_inv' _, simp }
 
-protected lemma model_with_corners.left_inverse : function.left_inverse I.symm I := I.left_inv
+protected lemma left_inverse : function.left_inverse I.symm I := I.left_inv
 
-@[simp, mfld_simps] lemma model_with_corners.symm_comp_self : I.symm ∘ I = id :=
+@[simp, mfld_simps] lemma symm_comp_self : I.symm ∘ I = id :=
 I.left_inverse.comp_eq_id
 
-protected lemma model_with_corners.right_inv_on : right_inv_on I.symm I (range I) :=
+protected lemma right_inv_on : right_inv_on I.symm I (range I) :=
 I.left_inverse.right_inv_on_range
 
-@[simp, mfld_simps] lemma model_with_corners.right_inv {x : E} (hx : x ∈ range I) :
-  I (I.symm x) = x :=
+@[simp, mfld_simps] protected lemma right_inv {x : E} (hx : x ∈ range I) : I (I.symm x) = x :=
 I.right_inv_on hx
 
-lemma model_with_corners.image (s : set H) :
-  I '' s = I.symm ⁻¹' s ∩ range I :=
+protected lemma image_eq (s : set H) : I '' s = I.symm ⁻¹' s ∩ range I :=
 begin
   refine (I.to_local_equiv.image_eq_target_inter_inv_preimage _).trans _,
   { rw I.source_eq, exact subset_univ _ },
   { rw [inter_comm, I.target_eq, I.to_local_equiv_coe_symm] }
 end
 
-protected lemma model_with_corners.closed_embedding : closed_embedding I :=
+protected lemma closed_embedding : closed_embedding I :=
 I.left_inverse.closed_embedding I.continuous_symm I.continuous
 
-lemma model_with_corners.closed_range : is_closed (range I) :=
+lemma closed_range : is_closed (range I) :=
 I.closed_embedding.closed_range
 
-lemma model_with_corners.map_nhds_eq (x : H) : map I (𝓝 x) = 𝓝[range I] (I x) :=
+lemma map_nhds_eq (x : H) : map I (𝓝 x) = 𝓝[range I] (I x) :=
 I.closed_embedding.to_embedding.map_nhds_eq x
 
-lemma model_with_corners.image_mem_nhds_within {x : H} {s : set H} (hs : s ∈ 𝓝 x) :
+lemma image_mem_nhds_within {x : H} {s : set H} (hs : s ∈ 𝓝 x) :
   I '' s ∈ 𝓝[range I] (I x) :=
 I.map_nhds_eq x ▸ image_mem_map hs
 
-lemma model_with_corners.symm_map_nhds_within_range (x : H) :
+lemma symm_map_nhds_within_range (x : H) :
   map I.symm (𝓝[range I] (I x)) = 𝓝 x :=
 by rw [← I.map_nhds_eq, map_map, I.symm_comp_self, map_id]
 
-lemma model_with_corners.unique_diff_preimage {s : set H} (hs : is_open s) :
+lemma unique_diff_preimage {s : set H} (hs : is_open s) :
   unique_diff_on 𝕜 (I.symm ⁻¹' s ∩ range I) :=
 by { rw inter_comm, exact I.unique_diff.inter (hs.preimage I.continuous_inv_fun) }
 
-lemma model_with_corners.unique_diff_preimage_source {β : Type*} [topological_space β]
+lemma unique_diff_preimage_source {β : Type*} [topological_space β]
   {e : local_homeomorph H β} : unique_diff_on 𝕜 (I.symm ⁻¹' (e.source) ∩ range I) :=
 I.unique_diff_preimage e.open_source
 
-lemma model_with_corners.unique_diff_at_image {x : H} : unique_diff_within_at 𝕜 (range I) (I x) :=
+lemma unique_diff_at_image {x : H} : unique_diff_within_at 𝕜 (range I) (I x) :=
 I.unique_diff _ (mem_range_self _)
 
-lemma model_with_corners.locally_compact [locally_compact_space E] (I : model_with_corners 𝕜 E H) :
+protected lemma locally_compact [locally_compact_space E] (I : model_with_corners 𝕜 E H) :
   locally_compact_space H :=
 begin
   have : ∀ (x : H), (𝓝 x).has_basis (λ s, s ∈ 𝓝 (I x) ∧ is_compact s)
@@ -268,6 +252,23 @@ begin
   exact (hsc.inter_right I.closed_range).image I.continuous_symm
 end
 
+end model_with_corners
+
+section
+variables (𝕜 E)
+
+/-- In the trivial model with corners, the associated local equiv is the identity. -/
+@[simp, mfld_simps] lemma model_with_corners_self_local_equiv :
+  (model_with_corners_self 𝕜 E).to_local_equiv = local_equiv.refl E := rfl
+
+@[simp, mfld_simps] lemma model_with_corners_self_coe :
+  (model_with_corners_self 𝕜 E : E → E) = id := rfl
+
+@[simp, mfld_simps] lemma model_with_corners_self_coe_symm :
+  ((model_with_corners_self 𝕜 E).symm : E → E) = id := rfl
+
+end
+
 end
 
 section model_with_corners_prod
@@ -307,7 +308,7 @@ as the model to tangent bundles. -/
   {𝕜 : Type u} [nondiscrete_normed_field 𝕜]
   {E : Type v} [normed_group E] [normed_space 𝕜 E] {H : Type w} [topological_space H]
   (I : model_with_corners 𝕜 E H) : model_with_corners 𝕜 (E × E) (model_prod H E) :=
- I.prod (model_with_corners_self 𝕜 E)
+I.prod (model_with_corners_self 𝕜 E)
 
 variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
 {E : Type*} [normed_group E] [normed_space 𝕜 E] {E' : Type*} [normed_group E'] [normed_space 𝕜 E']
@@ -496,14 +497,12 @@ begin
   split;
   simp only [local_equiv.prod_source, local_homeomorph.prod_to_local_equiv],
   { have h3 := times_cont_diff_on.prod_map he he',
-    rw [← model_with_corners.image I _, ← model_with_corners.image I' _,
-    set.prod_image_image_eq] at h3,
-    rw ← model_with_corners.image (I.prod I') _,
+    rw [← I.image_eq, ← I'.image_eq, set.prod_image_image_eq] at h3,
+    rw ← (I.prod I').image_eq,
     exact h3, },
   { have h3 := times_cont_diff_on.prod_map he_symm he'_symm,
-    rw [← model_with_corners.image I _, ← model_with_corners.image I' _,
-    set.prod_image_image_eq] at h3,
-    rw ← model_with_corners.image (I.prod I') _,
+    rw [← I.image_eq, ← I'.image_eq, set.prod_image_image_eq] at h3,
+    rw ← (I.prod I').image_eq,
     exact h3, }
 end
 

src/geometry/manifold/times_cont_mdiff.lean

@@ -1039,7 +1039,7 @@ begin
   let x : H := I.symm (0 : E),
   let y : H' := I'.symm (0 : E'),
   have A := hf.2 x y,
-  simp only [I.image, inter_comm] with mfld_simps at A ⊢,
+  simp only [I.image_eq, inter_comm] with mfld_simps at A ⊢,
   apply A.continuous_on_fderiv_within _ hn,
   convert hs.unique_diff_on x using 1,
   simp only [inter_comm] with mfld_simps

src/topology/algebra/module.lean

@@ -1083,6 +1083,11 @@ rfl
   (e₂.trans e₁).symm c = e₂.symm (e₁.symm c) :=
 rfl
 
+@[simp] theorem symm_image_image (e : M ≃L[R] M₂) (s : set M) : e.symm '' (e '' s) = s :=
+e.to_linear_equiv.to_equiv.symm_image_image s
+@[simp] theorem image_symm_image (e : M ≃L[R] M₂) (s : set M₂) : e '' (e.symm '' s) = s :=
+e.symm.symm_image_image s
+
 @[simp, norm_cast]
 lemma comp_coe (f : M ≃L[R] M₂) (f' : M₂ ≃L[R] M₃) :
   (f' : M₂ →L[R] M₃).comp (f : M →L[R] M₂) = (f.trans f' : M →L[R] M₃) :=

src/topology/homeomorph.lean

@@ -28,7 +28,7 @@ instance : has_coe_to_fun (α ≃ₜ β) := ⟨λ_, α → β, λe, e.to_equiv
   ((homeomorph.mk a b c) : α → β) = a :=
 rfl
 
-lemma coe_eq_to_equiv (h : α ≃ₜ β) (a : α) : h a = h.to_equiv a := rfl
+@[simp] lemma coe_to_equiv (h : α ≃ₜ β) : ⇑h.to_equiv = h := rfl
 
 lemma to_equiv_injective : function.injective (to_equiv : α ≃ₜ β → α ≃ β)
 | ⟨e, h₁, h₂⟩ ⟨e', h₁', h₂'⟩ rfl := rfl