refactor(data/set/function): move function.restrict to set, redefine (#2243)

urkud · kim-em · mergify[bot] · web-flow · commit 0fc4e6a8e194 · 2020-03-26T13:38:06.000Z
* refactor(data/set/function): move `function.restrict` to `set`, redefine

We had `subtype.restrict` and `function.restrict` both defined in the
same way using `subtype.val`. This PR moves `function.restrict` to
`set.restrict` and makes it use `coe` instead of `subtype.val`.

* Fix compile

* Update src/data/set/function.lean

Co-authored-by: Scott Morrison &lt;scott@tqft.net&gt;
Co-authored-by: mergify[bot] &lt;37929162+mergify[bot]@users.noreply.github.com&gt;
diff --git a/archive/sensitivity.lean b/archive/sensitivity.lean
@@ -373,7 +373,7 @@ begin
     rw ← dim_eq_injective (g m) g_injective,
     apply dim_V },
   have dimW : dim W = card H,
-  { have li : linear_independent ℝ (restrict e H) :=
+  { have li : linear_independent ℝ (set.restrict e H) :=
       linear_independent.comp (dual_pair_e_ε _).is_basis.1 _ subtype.val_injective,
     have hdW := dim_span li,
     rw set.range_restrict at hdW,
diff --git a/src/analysis/complex/exponential.lean b/src/analysis/complex/exponential.lean
@@ -1765,7 +1765,7 @@ begin
     have : δ ≤ ε ^ (1 / q) := le_trans (min_le_left _ _) (min_le_right _ _),
     have : δ < 1 := lt_of_le_of_lt (min_le_right _ _) (by norm_num),
     use δ, use δ0, rintros ⟨⟨x, y⟩, hy⟩,
-    simp only [subtype.dist_eq, real.dist_eq, prod.dist_eq, sub_zero],
+    simp only [subtype.dist_eq, real.dist_eq, prod.dist_eq, sub_zero, subtype.coe_mk],
     assume h, rw max_lt_iff at h, cases h with xδ yy₀,
     have qy : q < y, calc q < y₀ / 2 : q_lt
       ... = y₀ - y₀ / 2 : (sub_half _).symm
diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean
@@ -1432,7 +1432,7 @@ set.ext $ assume a,
 ⟨assume ⟨⟨a', ha'⟩, in_s, h_eq⟩, h_eq ▸ ⟨ha', in_s⟩,
   assume ⟨ha, in_s⟩, ⟨⟨a, ha⟩, in_s, rfl⟩⟩
 
-lemma val_range {p : α → Prop} :
+@[simp] lemma val_range {p : α → Prop} :
   set.range (@subtype.val _ p) = {x | p x} :=
 by rw ← set.image_univ; simp [-set.image_univ, val_image]
 
@@ -1478,13 +1478,13 @@ section range
 
 variable {α : Type*}
 
-@[simp] lemma subtype.val_range {p : α → Prop} :
-  range (@subtype.val _ p) = {x | p x} :=
-subtype.val_range
-
 @[simp] lemma range_coe_subtype (s : set α) : range (coe : s → α) = s :=
 subtype.val_range
 
+theorem preimage_coe_eq_preimage_coe_iff {s t u : set α} :
+  ((coe : s → α) ⁻¹' t = coe ⁻¹' u) ↔ t ∩ s = u ∩ s :=
+subtype.preimage_val_eq_preimage_val_iff _ _ _
+
 end range
 
 /-! ### Lemmas about cartesian product of sets -/
diff --git a/src/data/set/countable.lean b/src/data/set/countable.lean
@@ -84,7 +84,7 @@ begin
   have : countable (univ : set s) := countable_encodable _,
   rcases countable_iff_exists_surjective.1 this with ⟨g, hg⟩,
   have : range g = univ := univ_subset_iff.1 hg,
-  use subtype.val ∘ g,
+  use coe ∘ g,
   rw [range_comp, this],
   simp
 end
diff --git a/src/data/set/function.lean b/src/data/set/function.lean
@@ -9,6 +9,8 @@ import data.set.basic logic.function
 
 ## Main definitions
 
+### Predicate
+
 * `eq_on f₁ f₂ s` : functions `f₁` and `f₂` are equal at every point of `s`;
 * `maps_to f s t` : `f` sends every point of `s` to a point of `t`;
 * `inj_on f s` : restriction of `f` to `s` is injective;
@@ -18,6 +20,13 @@ import data.set.basic logic.function
 * `right_inv_on f' f t` : for every `y ∈ t` we have `f (f' y) = y`;
 * `inv_on f' f s t` : `f'` is a two-side inverse of `f` on `s` and `t`, i.e.
   we have `left_inv_on f' f s` and `right_inv_on f' f t`.
+
+### Functions
+
+* `restrict f s` : restrict the domain of `f` to the set `s`;
+* `cod_restrict f s h` : given `h : ∀ x, f x ∈ s`, restrict the codomain of `f` to the set `s`;
+* `maps_to.restrict f s t h`: given `h : maps_to f s t`, restrict the domain of `f` to `s`
+  and the codomain to `t`.
 -/
 universes u v w x y
 
@@ -29,8 +38,25 @@ namespace set
 
 /-! ### Restrict -/
 
-lemma range_restrict (f : α → β) (s : set α) : set.range (restrict f s) = f '' s :=
-by { ext x, simp [restrict], refl }
+/-- Restrict domain of a function `f` to a set `s`. Same as `subtype.restrict` but this version
+takes an argument `↥s` instead of `subtype s`. -/
+def restrict (f : α → β) (s : set α) : s → β := λ x, f x
+
+lemma restrict_eq (f : α → β) (s : set α) : s.restrict f = f ∘ coe := rfl
+
+@[simp] lemma restrict_apply (f : α → β) (s : set α) (x : s) : restrict f s x = f x := rfl
+
+@[simp] lemma range_restrict (f : α → β) (s : set α) : set.range (restrict f s) = f '' s :=
+range_comp.trans $ congr_arg (('') f) s.range_coe_subtype
+
+/-- Restrict codomain of a function `f` to a set `s`. Same as `subtype.coind` but this version
+has codomain `↥s` instead of `subtype s`. -/
+def cod_restrict (f : α → β) (s : set β) (h : ∀ x, f x ∈ s) : α → s :=
+λ x, ⟨f x, h x⟩
+
+@[simp] lemma coe_cod_restrict_apply (f : α → β) (s : set β) (h : ∀ x, f x ∈ s) (x : α) :
+  (cod_restrict f s h x : β) = f x :=
+rfl
 
 variables {s s₁ s₂ : set α} {t t₁ t₂ : set β} {p : set γ} {f f₁ f₂ f₃ : α → β} {g : β → γ}
   {f' f₁' f₂' : β → α} {g' : γ → β}
diff --git a/src/data/subtype.lean b/src/data/subtype.lean
@@ -30,7 +30,7 @@ end subtype
 namespace subtype
 variables {α : Sort*} {β : Sort*} {γ : Sort*} {p : α → Prop}
 
-lemma val_eq_coe (x : subtype p) : x.val = x := rfl
+lemma val_eq_coe : @val _ p = coe := rfl
 
 protected lemma eq' : ∀ {a1 a2 : {x // p x}}, a1.val = a2.val → a1 = a2
 | ⟨x, h1⟩ ⟨.(x), h2⟩ rfl := rfl
diff --git a/src/linear_algebra/basis.lean b/src/linear_algebra/basis.lean
@@ -272,7 +272,7 @@ end
 
 lemma linear_independent.restrict_of_comp_subtype {s : set ι}
   (hs : linear_independent R (v ∘ subtype.val : s → M)) :
-  linear_independent R (function.restrict v s) :=
+  linear_independent R (s.restrict v) :=
 begin
   have h_restrict : restrict v s = v ∘ (λ x, x.val) := rfl,
   rw [linear_independent_iff, h_restrict, finsupp.total_comp],
@@ -1134,7 +1134,7 @@ begin
     rwa h₂ at h₁ },
   rcases exists_subset_is_basis this with ⟨C, BC, hC⟩,
   haveI : inhabited V := ⟨0⟩,
-  use hC.constr (function.restrict (inv_fun f) C : C → V),
+  use hC.constr (C.restrict (inv_fun f)),
   apply @is_basis.ext _ _ _ _ _ _ _ _ _ _ _ _ hB,
   intros b,
   rw image_subset_iff at BC,
@@ -1153,7 +1153,7 @@ lemma exists_right_inverse_linear_map_of_surjective {f : V →ₗ[K] V'}
 begin
   rcases exists_is_basis K V' with ⟨C, hC⟩,
   haveI : inhabited V := ⟨0⟩,
-  use hC.constr (function.restrict (inv_fun f) C : C → V),
+  use hC.constr (C.restrict (inv_fun f)),
   apply @is_basis.ext _ _ _ _ _ _ _ _ _ _ _ _ hC,
   intros c,
   simp [constr_basis hC],
diff --git a/src/logic/function.lean b/src/logic/function.lean
@@ -270,10 +270,6 @@ by funext ; refl
 lemma uncurry'_curry {α : Type*} {β : Type*} {γ : Type*} (f : α × β → γ) : uncurry' (curry f) = f :=
 by { funext, simp [curry, uncurry', prod.mk.eta] }
 
-def restrict {α β} (f : α → β) (s : set α) : subtype s → β := λ x, f x.val
-
-theorem restrict_eq {α β} (f : α → β) (s : set α) : function.restrict f s = f ∘ (@subtype.val _ s) := rfl
-
 section bicomp
 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {ε : Type*}
 
diff --git a/src/measure_theory/integration.lean b/src/measure_theory/integration.lean
@@ -13,7 +13,7 @@ import
   measure_theory.measure_space
   measure_theory.borel_space
 noncomputable theory
-open set filter
+open set (hiding restrict restrict_apply) filter
 open_locale classical topological_space
 
 namespace measure_theory
@@ -919,7 +919,7 @@ begin
     le_supr_of_le (s.restrict (- t)) $ le_supr_of_le _ _),
   { assume a,
     by_cases a ∈ t;
-      simp [h, simple_func.restrict_apply, ht.compl],
+      simp [h, restrict_apply, ht.compl],
     exact le_trans (hfs a) (by_contradiction $ assume hnfg, h (hts hnfg)) },
   { refine le_of_eq (s.integral_congr _ _),
     filter_upwards [this],
diff --git a/src/topology/constructions.lean b/src/topology/constructions.lean
@@ -40,7 +40,7 @@ variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
 section constructions
 
 instance {p : α → Prop} [t : topological_space α] : topological_space (subtype p) :=
-induced subtype.val t
+induced coe t
 
 instance {r : α → α → Prop} [t : topological_space α] : topological_space (quot r) :=
 coinduced (quot.mk r) t
@@ -383,7 +383,7 @@ lemma is_open.is_open_map_subtype_val {s : set α} (hs : is_open s) :
 hs.open_embedding_subtype_val.is_open_map
 
 lemma is_open_map.restrict {f : α → β} (hf : is_open_map f) {s : set α} (hs : is_open s) :
-  is_open_map (function.restrict f s) :=
+  is_open_map (s.restrict f) :=
 hf.comp hs.is_open_map_subtype_val
 
 lemma is_closed.closed_embedding_subtype_val {s : set α} (hs : is_closed s) :
diff --git a/src/topology/continuous_on.lean b/src/topology/continuous_on.lean
@@ -198,9 +198,8 @@ begin
 end
 
 theorem tendsto_nhds_within_iff_subtype {s : set α} {a : α} (h : a ∈ s) (f : α → β) (l : filter β) :
-  tendsto f (nhds_within a s) l ↔ tendsto (function.restrict f s) (𝓝 ⟨a, h⟩) l :=
-by rw [tendsto, tendsto, function.restrict, nhds_within_eq_map_subtype_val h,
-    ←(@filter.map_map _ _ _ _ subtype.val)]
+  tendsto f (nhds_within a s) l ↔ tendsto (s.restrict f) (𝓝 ⟨a, h⟩) l :=
+by { simp only [tendsto, nhds_within_eq_map_subtype_val h, filter.map_map], refl }
 
 variables [topological_space β] [topological_space γ]
 
@@ -228,7 +227,7 @@ theorem continuous_within_at_univ (f : α → β) (x : α) :
 by rw [continuous_at, continuous_within_at, nhds_within_univ]
 
 theorem continuous_within_at_iff_continuous_at_restrict (f : α → β) {x : α} {s : set α} (h : x ∈ s) :
-  continuous_within_at f s x ↔ continuous_at (function.restrict f s) ⟨x, h⟩ :=
+  continuous_within_at f s x ↔ continuous_at (s.restrict f) ⟨x, h⟩ :=
 tendsto_nhds_within_iff_subtype h f _
 
 theorem continuous_within_at.tendsto_nhds_within_image {f : α → β} {x : α} {s : set α}
@@ -244,7 +243,7 @@ theorem continuous_on_iff {f : α → β} {s : set α} :
 by simp only [continuous_on, continuous_within_at, tendsto_nhds, mem_nhds_within]
 
 theorem continuous_on_iff_continuous_restrict {f : α → β} {s : set α} :
-  continuous_on f s ↔ continuous (function.restrict f s) :=
+  continuous_on f s ↔ continuous (s.restrict f) :=
 begin
   rw [continuous_on, continuous_iff_continuous_at], split,
   { rintros h ⟨x, xs⟩,
@@ -255,22 +254,22 @@ end
 
 theorem continuous_on_iff' {f : α → β} {s : set α} :
   continuous_on f s ↔ ∀ t : set β, is_open t → ∃ u, is_open u ∧ f ⁻¹' t ∩ s = u ∩ s :=
-have ∀ t, is_open (function.restrict f s ⁻¹' t) ↔ ∃ (u : set α), is_open u ∧ f ⁻¹' t ∩ s = u ∩ s,
+have ∀ t, is_open (s.restrict f ⁻¹' t) ↔ ∃ (u : set α), is_open u ∧ f ⁻¹' t ∩ s = u ∩ s,
   begin
     intro t,
-    rw [is_open_induced_iff, function.restrict_eq, set.preimage_comp],
-    simp only [subtype.preimage_val_eq_preimage_val_iff],
+    rw [is_open_induced_iff, set.restrict_eq, set.preimage_comp],
+    simp only [preimage_coe_eq_preimage_coe_iff],
     split; { rintros ⟨u, ou, useq⟩, exact ⟨u, ou, useq.symm⟩ }
   end,
 by rw [continuous_on_iff_continuous_restrict, continuous]; simp only [this]
 
 theorem continuous_on_iff_is_closed {f : α → β} {s : set α} :
   continuous_on f s ↔ ∀ t : set β, is_closed t → ∃ u, is_closed u ∧ f ⁻¹' t ∩ s = u ∩ s :=
-have ∀ t, is_closed (function.restrict f s ⁻¹' t) ↔ ∃ (u : set α), is_closed u ∧ f ⁻¹' t ∩ s = u ∩ s,
+have ∀ t, is_closed (s.restrict f ⁻¹' t) ↔ ∃ (u : set α), is_closed u ∧ f ⁻¹' t ∩ s = u ∩ s,
   begin
     intro t,
-    rw [is_closed_induced_iff, function.restrict_eq, set.preimage_comp],
-    simp only [subtype.preimage_val_eq_preimage_val_iff]
+    rw [is_closed_induced_iff, set.restrict_eq, set.preimage_comp],
+    simp only [preimage_coe_eq_preimage_coe_iff]
   end,
 by rw [continuous_on_iff_continuous_restrict, continuous_iff_is_closed]; simp only [this]
 
@@ -324,7 +323,7 @@ begin
 end
 
 theorem is_open_map.continuous_on_image_of_left_inv_on {f : α → β} {s : set α}
-  (h : is_open_map (function.restrict f s)) {finv : β → α} (hleft : left_inv_on finv f s) :
+  (h : is_open_map (s.restrict f)) {finv : β → α} (hleft : left_inv_on finv f s) :
   continuous_on finv (f '' s) :=
 begin
   rintros _ ⟨x, xs, rfl⟩ t ht,
diff --git a/src/topology/metric_space/antilipschitz.lean b/src/topology/metric_space/antilipschitz.lean
@@ -22,6 +22,7 @@ we do not have a `posreal` type.
 variables {α : Type*} {β : Type*} {γ : Type*}
 
 open_locale nnreal
+open set
 
 /-- We say that `f : α → β` is `antilipschitz_with K` if for any two points `x`, `y` we have
 `K * edist x y ≤ edist (f x) (f y)`. -/
@@ -63,7 +64,7 @@ begin
   exact hf x y
 end
 
-lemma id : antilipschitz_with 1 (id : α → α) :=
+protected lemma id : antilipschitz_with 1 (id : α → α) :=
 λ x y, by simp only [ennreal.coe_one, one_mul, id, le_refl]
 
 lemma comp {Kg : ℝ≥0} {g : β → γ} (hg : antilipschitz_with Kg g)
@@ -74,6 +75,25 @@ calc edist x y ≤ Kf * edist (f x) (f y) : hf x y
 ... ≤ Kf * (Kg * edist (g (f x)) (g (f y))) : ennreal.mul_left_mono (hg _ _)
 ... = _ : by rw [ennreal.coe_mul, mul_assoc]
 
+lemma restrict (hf : antilipschitz_with K f) (s : set α) :
+  antilipschitz_with K (s.restrict f) :=
+λ x y, hf x y
+
+lemma cod_restrict (hf : antilipschitz_with K f) {s : set β} (hs : ∀ x, f x ∈ s) :
+  antilipschitz_with K (s.cod_restrict f hs) :=
+λ x y, hf x y
+
+lemma to_right_inv_on' {s : set α} (hf : antilipschitz_with K (s.restrict f))
+  {g : β → α} {t : set β} (g_maps : maps_to g t s) (g_inv : right_inv_on g f t) :
+  lipschitz_with K (t.restrict g) :=
+λ x y, by simpa only [restrict_apply, g_inv x.mem, g_inv y.mem, subtype.edist_eq, subtype.coe_mk]
+  using hf ⟨g x, g_maps x.mem⟩ ⟨g y, g_maps y.mem⟩
+
+lemma to_right_inv_on (hf : antilipschitz_with K f) {g : β → α} {t : set β}
+  (h : right_inv_on g f t) :
+  lipschitz_with K (t.restrict g) :=
+(hf.restrict univ).to_right_inv_on' (maps_to_univ g t) h
+
 lemma to_inverse (hf : antilipschitz_with K f) {g : β → α} (hg : function.right_inverse g f) :
   lipschitz_with K g :=
 begin
@@ -96,6 +116,9 @@ begin
       rwa mul_comm } }
 end
 
+lemma subtype_coe (s : set α) : antilipschitz_with 1 (coe : s → α) :=
+antilipschitz_with.id.restrict s
+
 lemma of_subsingleton [subsingleton α] {K : ℝ≥0} : antilipschitz_with K f :=
 λ x y, by simp only [subsingleton.elim x y, edist_self, zero_le]
 
diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean
@@ -832,9 +832,9 @@ def metric_space.induced {α β} (f : α → β) (hf : function.injective f)
 
 instance subtype.metric_space {α : Type*} {p : α → Prop} [t : metric_space α] :
   metric_space (subtype p) :=
-metric_space.induced subtype.val (λ x y, subtype.eq) t
+metric_space.induced coe (λ x y, subtype.coe_ext.2) t
 
-theorem subtype.dist_eq {p : α → Prop} (x y : subtype p) : dist x y = dist x.1 y.1 := rfl
+theorem subtype.dist_eq {p : α → Prop} (x y : subtype p) : dist x y = dist (x : α) y := rfl
 
 section nnreal
 
diff --git a/src/topology/metric_space/contracting.lean b/src/topology/metric_space/contracting.lean
@@ -168,8 +168,7 @@ begin
   { convert (continuous_subtype_coe.tendsto _).comp h_tendsto, ext n,
     simp only [(∘), maps_to.iterate_restrict, maps_to.coe_restrict_apply, subtype.coe_mk] },
   { convert hle n,
-    rw [maps_to.iterate_restrict, eq_comm, subtype.val_eq_coe, maps_to.coe_restrict_apply,
-      subtype.coe_mk] }
+    rw [maps_to.iterate_restrict, eq_comm, maps_to.coe_restrict_apply, subtype.coe_mk] }
 end
 
 variable (f) -- avoid `efixed_point _` in pretty printer
diff --git a/src/topology/metric_space/emetric_space.lean b/src/topology/metric_space/emetric_space.lean
@@ -384,11 +384,11 @@ def emetric_space.induced {α β} (f : α → β) (hf : function.injective f)
 
 /-- Emetric space instance on subsets of emetric spaces -/
 instance {α : Type*} {p : α → Prop} [t : emetric_space α] : emetric_space (subtype p) :=
-t.induced subtype.val (λ x y, subtype.eq)
+t.induced coe (λ x y, subtype.coe_ext.2)
 
 /-- The extended distance on a subset of an emetric space is the restriction of
 the original distance, by definition -/
-theorem subtype.edist_eq {p : α → Prop} (x y : subtype p) : edist x y = edist x.1 y.1 := rfl
+theorem subtype.edist_eq {p : α → Prop} (x y : subtype p) : edist x y = edist (x : α) y := rfl
 
 /-- The product of two emetric spaces, with the max distance, is an extended
 metric spaces. We make sure that the uniform structure thus constructed is the one
diff --git a/src/topology/metric_space/lipschitz.lean b/src/topology/metric_space/lipschitz.lean
@@ -110,6 +110,10 @@ lipschitz_with.of_edist_le $ assume x y, le_refl _
 protected lemma subtype_coe (s : set α) : lipschitz_with 1 (coe : s → α) :=
 lipschitz_with.subtype_val s
 
+protected lemma restrict (hf : lipschitz_with K f) (s : set α) :
+  lipschitz_with K (s.restrict f) :=
+λ x y, hf x y
+
 protected lemma comp {Kf Kg : ℝ≥0} {f : β → γ} {g : α → β}
   (hf : lipschitz_with Kf f) (hg : lipschitz_with Kg g) : lipschitz_with (Kf * Kg) (f ∘ g) :=
 assume x y,
