feat(topology/local_homeomorph): add is_image, piecewise, and disjoint_union (#6804)

Also add `local_equiv.copy` and `local_homeomorph.replace_equiv` and use them for `local_equiv.disjoint_union` and `local_homeomorph.disjoint_union.

Author: urkud

src/data/equiv/local_equiv.lean

@@ -192,6 +192,24 @@ protected lemma inj_on : inj_on e e.source := e.left_inv_on.inj_on
 protected lemma bij_on : bij_on e e.source e.target := e.inv_on.bij_on e.maps_to e.symm_maps_to
 protected lemma surj_on : surj_on e e.source e.target := e.bij_on.surj_on
 
+/-- Create a copy of a `local_equiv` providing better definitional equalities. -/
+@[simps] def copy (e : local_equiv α β) (f : α → β) (hf : ⇑e = f) (g : β → α) (hg : ⇑e.symm = g)
+  (s : set α) (hs : e.source = s) (t : set β) (ht : e.target = t) :
+  local_equiv α β :=
+{ to_fun := f,
+  inv_fun := g,
+  source := s,
+  target := t,
+  map_source' := λ x, ht ▸ hs ▸ hf ▸ e.map_source,
+  map_target' := λ y, hs ▸ ht ▸ hg ▸ e.map_target,
+  left_inv' := λ x, hs ▸ hf ▸ hg ▸ e.left_inv,
+  right_inv' := λ x, ht ▸ hf ▸ hg ▸ e.right_inv }
+
+lemma copy_eq_self (e : local_equiv α β) (f : α → β) (hf : ⇑e = f) (g : β → α) (hg : ⇑e.symm = g)
+  (s : set α) (hs : e.source = s) (t : set β) (ht : e.target = t) :
+  e.copy f hf g hg s hs t ht = e :=
+by { substs f g s t, cases e, refl }
+
 /-- Associating to a local_equiv an equiv between the source and the target -/
 protected def to_equiv : equiv (e.source) (e.target) :=
 { to_fun    := λ x, ⟨e x, e.map_source x.mem⟩,
@@ -292,10 +310,33 @@ begin
       e'.left_inv he] }
 end
 
+lemma inter_eq_of_inter_eq_of_eq_on {e' : local_equiv α β} (h : e.is_image s t)
+  (h' : e'.is_image s t) (hs : e.source ∩ s = e'.source ∩ s) (Heq : eq_on e e' (e.source ∩ s)) :
+  e.target ∩ t = e'.target ∩ t :=
+by rw [← h.image_eq, ← h'.image_eq, ← hs, Heq.image_eq]
+
+lemma symm_eq_on_of_inter_eq_of_eq_on {e' : local_equiv α β} (h : e.is_image s t)
+  (hs : e.source ∩ s = e'.source ∩ s) (Heq : eq_on e e' (e.source ∩ s)) :
+  eq_on e.symm e'.symm (e.target ∩ t) :=
+begin
+  rw [← h.image_eq],
+  rintros y ⟨x, hx, rfl⟩,
+  have hx' := hx, rw hs at hx',
+  rw [e.left_inv hx.1, Heq hx, e'.left_inv hx'.1]
+end
+
 end is_image
 
 lemma is_image_source_target : e.is_image e.source e.target := λ x hx, by simp [hx]
 
+lemma is_image_source_target_of_disjoint (e' : local_equiv α β) (hs : disjoint e.source e'.source)
+  (ht : disjoint e.target e'.target) :
+  e.is_image e'.source e'.target :=
+assume x hx,
+have x ∉ e'.source, from λ hx', hs ⟨hx, hx'⟩,
+have e x ∉ e'.target, from λ hx', ht ⟨e.maps_to hx, hx'⟩,
+by simp only *
+
 lemma image_source_inter_eq' (s : set α) :
   e '' (e.source ∩ s) = e.target ∩ e.symm ⁻¹' s :=
 by rw [inter_comm, e.left_inv_on.image_inter', image_source_eq_target, inter_comm]
@@ -353,7 +394,7 @@ end
 
 /-- Restricting a local equivalence to e.source ∩ s -/
 protected def restr (s : set α) : local_equiv α β :=
-(@is_image.of_symm_preimage_eq α β e s _ rfl).restr
+(@is_image.of_symm_preimage_eq α β e s (e.symm ⁻¹' s) rfl).restr
 
 @[simp, mfld_simps] lemma restr_coe (s : set α) : (e.restr s : α → β) = e := rfl
 @[simp, mfld_simps] lemma restr_coe_symm (s : set α) : ((e.restr s).symm : β → α) = e.symm := rfl
@@ -626,38 +667,23 @@ lemma symm_piecewise (e e' : local_equiv α β) {s : set α} {t : set β}
   (e.piecewise e' s t H H').symm = e.symm.piecewise e'.symm t s H.symm H'.symm :=
 rfl
 
-/-- Combine two `local_equiv`s with disjoint sources and disjoint targets. We do not reuse
-`local_equiv.piecewise` here to provide better formulas for `source` and `target`. -/
+/-- Combine two `local_equiv`s with disjoint sources and disjoint targets. We reuse
+`local_equiv.piecewise`, then override `source` and `target` to ensure better definitional
+equalities. -/
 @[simps] def disjoint_union (e e' : local_equiv α β) (hs : disjoint e.source e'.source)
   (ht : disjoint e.target e'.target) [∀ x, decidable (x ∈ e.source)]
   [∀ y, decidable (y ∈ e.target)] :
   local_equiv α β :=
-{ to_fun := e.source.piecewise e e',
-  inv_fun := e.target.piecewise e.symm e'.symm,
-  source := e.source ∪ e'.source,
-  target := e.target ∪ e'.target,
-  map_source' := λ x,
-    have x ∈ e'.source → x ∉ e.source, from λ h' h, hs ⟨h, h'⟩,
-    by rintro (he|he'); simp *,
-  map_target' := λ y,
-    have y ∈ e'.target → y ∉ e.target, from λ h' h, ht ⟨h, h'⟩,
-    by rintro (he|he'); simp *,
-  left_inv' := λ x,
-    begin
-      rintro (he|he'),
-      { simp * },
-      { have : x ∉ e.source ∧ e' x ∉ e.target,
-          from ⟨λ h, hs ⟨h, he'⟩, λ h, ht ⟨h, e'.map_source he'⟩⟩,
-        simp * }
-    end,
-  right_inv' := λ y,
-    begin
-      rintro (he|he'),
-      { simp * },
-      { have : y ∉ e.target ∧ e'.symm y ∉ e.source,
-          from ⟨λ h, ht ⟨h, he'⟩, λ h, hs ⟨h, e'.map_target he'⟩⟩,
-        simp * }
-    end }
+(e.piecewise e' e.source e.target e.is_image_source_target $
+  e'.is_image_source_target_of_disjoint _ hs.symm ht.symm).copy
+  _ rfl _ rfl (e.source ∪ e'.source) (ite_left _ _) (e.target ∪ e'.target) (ite_left _ _)
+
+lemma disjoint_union_eq_piecewise (e e' : local_equiv α β) (hs : disjoint e.source e'.source)
+  (ht : disjoint e.target e'.target) [∀ x, decidable (x ∈ e.source)]
+  [∀ y, decidable (y ∈ e.target)] :
+  e.disjoint_union e' hs ht = e.piecewise e' e.source e.target e.is_image_source_target
+    (e'.is_image_source_target_of_disjoint _ hs.symm ht.symm) :=
+copy_eq_self _ _ _ _ _ _ _ _ _
 
 section pi
 

src/data/set/basic.lean

@@ -960,10 +960,10 @@ lemma insert_diff_self_of_not_mem {a : α} {s : set α} (h : a ∉ s) :
   insert a s \ {a} = s :=
 by { ext, simp [and_iff_left_of_imp (λ hx : x ∈ s, show x ≠ a, from λ hxa, h $ hxa ▸ hx)] }
 
-theorem union_diff_self {s t : set α} : s ∪ (t \ s) = s ∪ t :=
+@[simp] theorem union_diff_self {s t : set α} : s ∪ (t \ s) = s ∪ t :=
 by finish [ext_iff, iff_def]
 
-theorem diff_union_self {s t : set α} : (s \ t) ∪ t = s ∪ t :=
+@[simp] theorem diff_union_self {s t : set α} : (s \ t) ∪ t = s ∪ t :=
 by rw [union_comm, union_diff_self, union_comm]
 
 theorem diff_inter_self {a b : set α} : (b \ a) ∩ a = ∅ :=
@@ -1043,6 +1043,10 @@ ite_inter_compl_self t s s'
 
 @[simp] lemma ite_same (t s : set α) : t.ite s s = s := inter_union_diff _ _
 
+@[simp] lemma ite_left (s t : set α) : s.ite s t = s ∪ t := by simp [set.ite]
+
+@[simp] lemma ite_right (s t : set α) : s.ite t s = t ∩ s := by simp [set.ite]
+
 @[simp] lemma ite_empty (s s' : set α) : set.ite ∅ s s' = s' :=
 by simp [set.ite]
 
@@ -1073,6 +1077,17 @@ lemma ite_inter (t s₁ s₂ s : set α) :
   t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s :=
 by rw [ite_inter_inter, ite_same]
 
+lemma ite_inter_of_inter_eq (t : set α) {s₁ s₂ s : set α} (h : s₁ ∩ s = s₂ ∩ s) :
+  t.ite s₁ s₂ ∩ s = s₁ ∩ s :=
+by rw [← ite_inter, ← h, ite_same]
+
+lemma subset_ite {t s s' u : set α} : u ⊆ t.ite s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s' :=
+begin
+  simp only [subset_def, ← forall_and_distrib],
+  refine forall_congr (λ x, _),
+  by_cases hx : x ∈ t; simp [*, set.ite]
+end
+
 /-! ### Inverse image -/
 
 /-- The preimage of `s : set β` by `f : α → β`, written `f ⁻¹' s`,
@@ -1107,6 +1122,10 @@ theorem subset_preimage_univ {s : set α} : s ⊆ f ⁻¹' univ := subset_univ _
 @[simp] theorem preimage_diff (f : α → β) (s t : set β) :
   f ⁻¹' (s \ t) = f ⁻¹' s \ f ⁻¹' t := rfl
 
+@[simp] theorem preimage_ite (f : α → β) (s t₁ t₂ : set β) :
+  f ⁻¹' (s.ite t₁ t₂) = (f ⁻¹' s).ite (f ⁻¹' t₁) (f ⁻¹' t₂) :=
+rfl
+
 @[simp] theorem preimage_set_of_eq {p : α → Prop} {f : β → α} : f ⁻¹' {a | p a} = {a | p (f a)} :=
 rfl
 

src/data/set/function.lean

@@ -73,6 +73,8 @@ variables {s s₁ s₂ : set α} {t t₁ t₂ : set β} {p : set γ} {f f₁ f
 @[reducible] def eq_on (f₁ f₂ : α → β) (s : set α) : Prop :=
 ∀ ⦃x⦄, x ∈ s → f₁ x = f₂ x
 
+@[simp] lemma eq_on_empty (f₁ f₂ : α → β) : eq_on f₁ f₂ ∅ := λ x, false.elim
+
 @[symm] lemma eq_on.symm (h : eq_on f₁ f₂ s) : eq_on f₂ f₁ s :=
 λ x hx, (h hx).symm
 
@@ -649,12 +651,10 @@ begin
 end
 
 @[simp, priority 990]
-lemma piecewise_eq_of_mem {i : α} (hi : i ∈ s) : s.piecewise f g i = f i :=
-by simp [piecewise, hi]
+lemma piecewise_eq_of_mem {i : α} (hi : i ∈ s) : s.piecewise f g i = f i := if_pos hi
 
 @[simp, priority 990]
-lemma piecewise_eq_of_not_mem {i : α} (hi : i ∉ s) : s.piecewise f g i = g i :=
-by simp [piecewise, hi]
+lemma piecewise_eq_of_not_mem {i : α} (hi : i ∉ s) : s.piecewise f g i = g i := if_neg hi
 
 lemma piecewise_singleton (x : α) [Π y, decidable (y ∈ ({x} : set α))] [decidable_eq α]
   (f g : α → β) : piecewise {x} f g = function.update g x (f x) :=

src/geometry/manifold/charted_space.lean

@@ -433,6 +433,7 @@ begin
     rintros e ⟨s, hs, hes⟩,
     refine G.eq_on_source _ hes,
     convert closed_under_restriction' G.id_mem hs,
+    change s = _ ∩ _,
     rw hs.interior_eq,
     simp only with mfld_simps },
   { intros h,

src/topology/basic.lean

@@ -438,6 +438,8 @@ lemma frontier_eq_closure_inter_closure {s : set α} :
   frontier s = closure s ∩ closure sᶜ :=
 by rw [closure_compl, frontier, diff_eq]
 
+lemma frontier_subset_closure {s : set α} : frontier s ⊆ closure s := diff_subset _ _
+
 /-- The complement of a set has the same frontier as the original set. -/
 @[simp] lemma frontier_compl (s : set α) : frontier sᶜ = frontier s :=
 by simp only [frontier_eq_closure_inter_closure, compl_compl, inter_comm]
@@ -467,6 +469,9 @@ by rw [frontier, hs.closure_eq]
 lemma is_open.frontier_eq {s : set α} (hs : is_open s) : frontier s = closure s \ s :=
 by rw [frontier, hs.interior_eq]
 
+lemma is_open.inter_frontier_eq {s : set α} (hs : is_open s) : s ∩ frontier s = ∅ :=
+by rw [hs.frontier_eq, inter_diff_self]
+
 /-- The frontier of a set is closed. -/
 lemma is_closed_frontier {s : set α} : is_closed (frontier s) :=
 by rw frontier_eq_closure_inter_closure; exact is_closed_inter is_closed_closure is_closed_closure
@@ -488,6 +493,15 @@ lemma closure_eq_interior_union_frontier (s : set α) : closure s = interior s 
 lemma closure_eq_self_union_frontier (s : set α) : closure s = s ∪ frontier s :=
 (union_diff_cancel' interior_subset subset_closure).symm
 
+lemma is_open.inter_frontier_eq_empty_of_disjoint {s t : set α} (ht : is_open t)
+  (hd : disjoint s t) :
+  t ∩ frontier s = ∅ :=
+begin
+  rw [inter_comm, ← subset_compl_iff_disjoint],
+  exact subset.trans frontier_subset_closure (closure_minimal (λ _, disjoint_left.1 hd)
+    (is_closed_compl_iff.2 ht))
+end
+
 /-!
 ### Neighborhoods
 -/

src/topology/continuous_on.lean

@@ -926,6 +926,35 @@ lemma is_open.ite {s s' t : set α} (hs : is_open s) (hs' : is_open s')
   is_open (t.ite s s') :=
 hs.ite' hs' $ λ x hx, by simpa [hx] using ext_iff.1 ht x
 
+lemma ite_inter_closure_eq_of_inter_frontier_eq {s s' t : set α}
+  (ht : s ∩ frontier t = s' ∩ frontier t) :
+  t.ite s s' ∩ closure t = s ∩ closure t :=
+by rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_union_distrib_left,
+  ite_inter_self, ite_inter_of_inter_eq _ ht]
+
+lemma ite_inter_closure_compl_eq_of_inter_frontier_eq {s s' t : set α}
+  (ht : s ∩ frontier t = s' ∩ frontier t) :
+  t.ite s s' ∩ closure tᶜ = s' ∩ closure tᶜ :=
+by { rw [← ite_compl, ite_inter_closure_eq_of_inter_frontier_eq], rwa [frontier_compl, eq_comm] }
+
+lemma continuous_on_piecewise_ite' {s s' t : set α} {f f' : α → β} [∀ x, decidable (x ∈ t)]
+  (h : continuous_on f (s ∩ closure t)) (h' : continuous_on f' (s' ∩ closure tᶜ))
+  (H : s ∩ frontier t = s' ∩ frontier t) (Heq : eq_on f f' (s ∩ frontier t)) :
+  continuous_on (t.piecewise f f') (t.ite s s') :=
+begin
+  apply continuous_on.piecewise,
+  { rwa ite_inter_of_inter_eq _ H },
+  { rwa ite_inter_closure_eq_of_inter_frontier_eq H },
+  { rwa ite_inter_closure_compl_eq_of_inter_frontier_eq H }
+end
+
+lemma continuous_on_piecewise_ite {s s' t : set α} {f f' : α → β} [∀ x, decidable (x ∈ t)]
+  (h : continuous_on f s) (h' : continuous_on f' s')
+  (H : s ∩ frontier t = s' ∩ frontier t) (Heq : eq_on f f' (s ∩ frontier t)) :
+  continuous_on (t.piecewise f f') (t.ite s s') :=
+continuous_on_piecewise_ite' (h.mono (inter_subset_left _ _)) (h'.mono (inter_subset_left _ _))
+  H Heq
+
 lemma continuous_on_fst {s : set (α × β)} : continuous_on prod.fst s :=
 continuous_fst.continuous_on