refactor(topology/{basic,continuous_on}): review continuous_if etc (#…

…6182)

* move `continuous_if` to `topology/continuous_on`, use weaker assumptions;
* add `piecewise` versions of various `if` lemmas;
* add a specialized `continuous_if_le` version;
* use dot notation for `continuous_on.if` and `continuous_on.if'`;
* minor golfing here and there.

src/order/filter/basic.lean

@@ -2217,21 +2217,24 @@ lemma tendsto.not_tendsto {f : α → β} {a : filter α} {b₁ b₂ : filter β
   ¬ tendsto f a b₂ :=
 λ hf', (tendsto_inf.2 ⟨hf, hf'⟩).ne_bot.ne hb.eq_bot
 
-lemma tendsto_if {l₁ : filter α} {l₂ : filter β}
-    {f g : α → β} {p : α → Prop} [decidable_pred p]
-    (h₀ : tendsto f (l₁ ⊓ 𝓟 p) l₂)
-    (h₁ : tendsto g (l₁ ⊓ 𝓟 { x | ¬ p x }) l₂) :
+lemma tendsto.if {l₁ : filter α} {l₂ : filter β} {f g : α → β} {p : α → Prop} [∀ x, decidable (p x)]
+  (h₀ : tendsto f (l₁ ⊓ 𝓟 {x | p x}) l₂) (h₁ : tendsto g (l₁ ⊓ 𝓟 { x | ¬ p x }) l₂) :
   tendsto (λ x, if p x then f x else g x) l₁ l₂ :=
 begin
-  revert h₀ h₁, simp only [tendsto_def, mem_inf_principal],
-  intros h₀ h₁ s hs,
-  apply mem_sets_of_superset (inter_mem_sets (h₀ s hs) (h₁ s hs)),
-  rintros x ⟨hp₀, hp₁⟩, simp only [mem_preimage],
-  by_cases h : p x,
-  { rw if_pos h, exact hp₀ h },
-  rw if_neg h, exact hp₁ h
+  simp only [tendsto_def, mem_inf_principal] at *,
+  intros s hs,
+  filter_upwards [h₀ s hs, h₁ s hs],
+  simp only [mem_preimage], intros x hp₀ hp₁,
+  split_ifs,
+  exacts [hp₀ h, hp₁ h]
 end
 
+lemma tendsto.piecewise {l₁ : filter α} {l₂ : filter β} {f g : α → β}
+  {s : set α} [∀ x, decidable (x ∈ s)]
+  (h₀ : tendsto f (l₁ ⊓ 𝓟 s) l₂) (h₁ : tendsto g (l₁ ⊓ 𝓟 sᶜ) l₂) :
+  tendsto (piecewise s f g) l₁ l₂ :=
+h₀.if h₁
+
 /-! ### Products of filters -/
 
 section prod

src/topology/algebra/ordered.lean

@@ -537,10 +537,26 @@ lemma frontier_lt_subset_eq (hf : continuous f) (hg : continuous g) :
 by rw ← frontier_compl;
    convert frontier_le_subset_eq hg hf; simp [ext_iff, eq_comm]
 
+lemma continuous_if_le [topological_space γ] [Π x, decidable (f x ≤ g x)]
+  {f' g' : β → γ} (hf : continuous f) (hg : continuous g)
+  (hf' : continuous_on f' {x | f x ≤ g x}) (hg' : continuous_on g' {x | g x ≤ f x})
+  (hfg : ∀ x, f x = g x → f' x = g' x) :
+  continuous (λ x, if f x ≤ g x then f' x else g' x) :=
+begin
+  refine continuous_if (λ a ha, hfg _ (frontier_le_subset_eq hf hg ha)) _ (hg'.mono _),
+  { rwa [(is_closed_le hf hg).closure_eq] },
+  { simp only [not_le], exact closure_lt_subset_le hg hf }
+end
+
+lemma continuous.if_le [topological_space γ] [Π x, decidable (f x ≤ g x)] {f' g' : β → γ}
+  (hf' : continuous f') (hg' : continuous g') (hf : continuous f) (hg : continuous g)
+  (hfg : ∀ x, f x = g x → f' x = g' x) :
+  continuous (λ x, if f x ≤ g x then f' x else g' x) :=
+continuous_if_le hf hg hf'.continuous_on hg'.continuous_on hfg
+
 @[continuity] lemma continuous.min (hf : continuous f) (hg : continuous g) :
   continuous (λb, min (f b) (g b)) :=
-have ∀b∈frontier {b | f b ≤ g b}, f b = g b, from assume b hb, frontier_le_subset_eq hf hg hb,
-continuous_if this hf hg
+hf.if_le hg hf hg (λ x, id)
 
 @[continuity] lemma continuous.max (hf : continuous f) (hg : continuous g) :
   continuous (λb, max (f b) (g b)) :=

src/topology/basic.lean

@@ -1069,43 +1069,6 @@ lemma continuous_iff_ultrafilter {f : α → β} :
   continuous f ↔ ∀ x (g : ultrafilter α), ↑g ≤ 𝓝 x → tendsto f g (𝓝 (f x)) :=
 by simp only [continuous_iff_continuous_at, continuous_at_iff_ultrafilter]
 
-/-- A piecewise defined function `if p then f else g` is continuous, if both `f` and `g`
-are continuous, and they coincide on the frontier (boundary) of the set `{a | p a}`. -/
-lemma continuous_if {p : α → Prop} {f g : α → β} {h : ∀a, decidable (p a)}
-  (hp : ∀a∈frontier {a | p a}, f a = g a) (hf : continuous f) (hg : continuous g) :
-  continuous (λa, @ite (p a) (h a) β (f a) (g a)) :=
-continuous_iff_is_closed.mpr $
-assume s hs,
-have (λa, ite (p a) (f a) (g a)) ⁻¹' s =
-    (closure {a | p a} ∩  f ⁻¹' s) ∪ (closure {a | ¬ p a} ∩ g ⁻¹' s),
-  from set.ext $ assume a,
-  classical.by_cases
-    (assume : a ∈ frontier {a | p a},
-      have hac : a ∈ closure {a | p a}, from this.left,
-      have hai : a ∈ closure {a | ¬ p a},
-        from have a ∈ (interior {a | p a})ᶜ, from this.right, by rwa [←closure_compl] at this,
-      by by_cases p a; simp [h, hp a this, hac, hai, iff_def] {contextual := tt})
-    (assume hf : a ∈ (frontier {a | p a})ᶜ,
-      classical.by_cases
-        (assume : p a,
-          have hc : a ∈ closure {a | p a}, from subset_closure this,
-          have hnc : a ∉ closure {a | ¬ p a},
-            by show a ∉ closure {a | p a}ᶜ; rw [closure_compl]; simpa [frontier, hc] using hf,
-          by simp [this, hc, hnc])
-        (assume : ¬ p a,
-          have hc : a ∈ closure {a | ¬ p a}, from subset_closure this,
-          have hnc : a ∉ closure {a | p a},
-            begin
-              have hc : a ∈ closure {a | p a}ᶜ, from hc,
-              simp [closure_compl] at hc,
-              simpa [frontier, hc] using hf
-            end,
-          by simp [this, hc, hnc])),
-by rw [this]; exact is_closed_union
-  (is_closed_inter is_closed_closure $ continuous_iff_is_closed.mp hf s hs)
-  (is_closed_inter is_closed_closure $ continuous_iff_is_closed.mp hg s hs)
-
-
 /-! ### Continuity and partial functions -/
 
 /-- Continuity of a partial function -/

src/topology/continuous_on.lean

@@ -189,12 +189,18 @@ lemma nhds_within_prod {α : Type*} [topological_space α] {β : Type*} [topolog
   (u.prod v) ∈ 𝓝[s.prod t] (a, b) :=
 by { rw nhds_within_prod_eq, exact prod_mem_prod hu hv, }
 
-theorem tendsto_if_nhds_within {f g : α → β} {p : α → Prop} [decidable_pred p]
+theorem filter.tendsto.piecewise_nhds_within {f g : α → β} {t : set α} [∀ x, decidable (x ∈ t)]
+  {a : α} {s : set α} {l : filter β}
+  (h₀ : tendsto f (𝓝[s ∩ t] a) l) (h₁ : tendsto g (𝓝[s ∩ tᶜ] a) l) :
+  tendsto (piecewise t f g) (𝓝[s] a) l :=
+by apply tendsto.piecewise; rwa ← nhds_within_inter'
+
+theorem filter.tendsto.if_nhds_within {f g : α → β} {p : α → Prop} [decidable_pred p]
     {a : α} {s : set α} {l : filter β}
-    (h₀ : tendsto f (𝓝[s ∩ p] a) l)
+    (h₀ : tendsto f (𝓝[s ∩ {x | p x}] a) l)
     (h₁ : tendsto g (𝓝[s ∩ {x | ¬ p x}] a) l) :
   tendsto (λ x, if p x then f x else g x) (𝓝[s] a) l :=
-by apply tendsto_if; rw [←nhds_within_inter']; assumption
+h₀.piecewise_nhds_within h₁
 
 lemma map_nhds_within (f : α → β) (a : α) (s : set α) :
   map f (𝓝[s] a) =
@@ -710,84 +716,120 @@ begin
   exact tendsto_bot,
 end
 
-lemma continuous_on_if' {s : set α} {p : α → Prop} {f g : α → β} {h : ∀a, decidable (p a)}
-  (hpf : ∀ a ∈ s ∩ frontier {a | p a},
-    tendsto f (nhds_within a $ s ∩ {a | p a}) (𝓝 $ if p a then f a else g a))
-  (hpg : ∀ a ∈ s ∩ frontier {a | p a},
-    tendsto g (nhds_within a $ s ∩ {a | ¬p a}) (𝓝 $ if p a then f a else g a))
-  (hf : continuous_on f $ s ∩ {a | p a}) (hg : continuous_on g $ s ∩ {a | ¬p a}) :
-  continuous_on (λ a, if p a then f a else g a) s :=
+lemma continuous_on.piecewise' {s t : set α} {f g : α → β} [∀ a, decidable (a ∈ t)]
+  (hpf : ∀ a ∈ s ∩ frontier t, tendsto f (𝓝[s ∩ t] a) (𝓝 (piecewise t f g a)))
+  (hpg : ∀ a ∈ s ∩ frontier t, tendsto g (𝓝[s ∩ tᶜ] a) (𝓝 (piecewise t f g a)))
+  (hf : continuous_on f $ s ∩ t) (hg : continuous_on g $ s ∩ tᶜ) :
+  continuous_on (piecewise t f g) s :=
 begin
-  set A := {a | p a},
-  set B := {a | ¬p a},
-  rw [← (inter_univ s), ← union_compl_self A],
   intros x hx,
-  by_cases hx' : x ∈ frontier A,
-  { have hx'' : x ∈ s ∩ frontier A, from ⟨hx.1, hx'⟩,
-    rw inter_union_distrib_left,
-    apply continuous_within_at.union,
-    { apply tendsto_nhds_within_congr,
-      { exact λ y ⟨hys, hyA⟩, (piecewise_eq_of_mem _ _ _ hyA).symm },
-      { apply_assumption,
-        exact hx'' } },
-    { apply tendsto_nhds_within_congr,
-      { exact λ y ⟨hys, hyA⟩, (piecewise_eq_of_not_mem _ _ _ hyA).symm },
-      { apply_assumption,
-        exact hx'' } } },
-  { rw inter_union_distrib_left at ⊢ hx,
+  by_cases hx' : x ∈ frontier t,
+  { exact (hpf x ⟨hx, hx'⟩).piecewise_nhds_within (hpg x ⟨hx, hx'⟩) },
+  { rw [← inter_univ s, ← union_compl_self t, inter_union_distrib_left] at hx ⊢,
     cases hx,
     { apply continuous_within_at.union,
-      { exact (hf x hx).congr
-          (λ y hy, piecewise_eq_of_mem _ _ _ hy.2)
-          (piecewise_eq_of_mem _ _ _ hx.2), },
-      { rw ← frontier_compl at hx',
-        have : x ∉ closure Aᶜ,
-          from λ h, hx' ⟨h, (λ (h' : x ∈ interior Aᶜ), interior_subset h' hx.2)⟩,
+      { exact (hf x hx).congr (λ y hy, piecewise_eq_of_mem _ _ _ hy.2)
+          (piecewise_eq_of_mem _ _ _ hx.2) },
+      { have : x ∉ closure tᶜ,
+          from λ h, hx' ⟨subset_closure hx.2, by rwa closure_compl at h⟩,
         exact continuous_within_at_of_not_mem_closure
           (λ h, this (closure_inter_subset_inter_closure _ _ h).2) } },
     { apply continuous_within_at.union,
-      { have : x ∉ closure A,
-          from (λ h, hx' ⟨h, (λ (h' : x ∈ interior A), hx.2 (interior_subset h'))⟩),
+      { have : x ∉ closure t,
+          from (λ h, hx' ⟨h, (λ (h' : x ∈ interior t), hx.2 (interior_subset h'))⟩),
         exact continuous_within_at_of_not_mem_closure
           (λ h, this (closure_inter_subset_inter_closure _ _ h).2) },
       { exact (hg x hx).congr
           (λ y hy, piecewise_eq_of_not_mem _ _ _ hy.2)
           (piecewise_eq_of_not_mem _ _ _ hx.2) } } }
 end
 
-lemma continuous_on_if {α β : Type*} [topological_space α] [topological_space β] {p : α → Prop}
-  {h : ∀a, decidable (p a)} {s : set α} {f g : α → β}
+lemma continuous_on.if' {s : set α} {p : α → Prop} {f g : α → β} [∀ a, decidable (p a)]
+  (hpf : ∀ a ∈ s ∩ frontier {a | p a},
+    tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 $ if p a then f a else g a))
+  (hpg : ∀ a ∈ s ∩ frontier {a | p a},
+    tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 $ if p a then f a else g a))
+  (hf : continuous_on f $ s ∩ {a | p a}) (hg : continuous_on g $ s ∩ {a | ¬p a}) :
+  continuous_on (λ a, if p a then f a else g a) s :=
+hf.piecewise' hpf hpg hg
+
+lemma continuous_on.if {α β : Type*} [topological_space α] [topological_space β] {p : α → Prop}
+  [∀ a, decidable (p a)] {s : set α} {f g : α → β}
   (hp : ∀ a ∈ s ∩ frontier {a | p a}, f a = g a) (hf : continuous_on f $ s ∩ closure {a | p a})
   (hg : continuous_on g $ s ∩ closure {a | ¬ p a}) :
   continuous_on (λa, if p a then f a else g a) s :=
 begin
-  apply continuous_on_if',
+  apply continuous_on.if',
   { rintros a ha,
     simp only [← hp a ha, if_t_t],
     apply tendsto_nhds_within_mono_left (inter_subset_inter_right s subset_closure),
-    exact (hf a ⟨ha.1, ha.2.1⟩).tendsto },
+    exact hf a ⟨ha.1, ha.2.1⟩ },
   { rintros a ha,
     simp only [hp a ha, if_t_t],
     apply tendsto_nhds_within_mono_left (inter_subset_inter_right s subset_closure),
     rcases ha with ⟨has, ⟨_, ha⟩⟩,
     rw [← mem_compl_iff, ← closure_compl] at ha,
-    apply (hg a ⟨has, ha⟩).tendsto, },
+    apply hg a ⟨has, ha⟩ },
   { exact hf.mono (inter_subset_inter_right s subset_closure) },
   { exact hg.mono (inter_subset_inter_right s subset_closure) }
 end
 
-lemma continuous_if' {p : α → Prop} {f g : α → β} {h : ∀a, decidable (p a)}
-  (hpf : ∀ a ∈ frontier {x | p x},
-    tendsto f (nhds_within a {x | p x}) (𝓝 $ ite (p a) (f a) (g a)))
-  (hpg : ∀ a ∈ frontier {x | p x},
-    tendsto g (nhds_within a {x | ¬p x}) (𝓝 $ ite (p a) (f a) (g a)))
+lemma continuous_on.piecewise {s t : set α} {f g : α → β} [∀ a, decidable (a ∈ t)]
+  (ht : ∀ a ∈ s ∩ frontier t, f a = g a) (hf : continuous_on f $ s ∩ closure t)
+  (hg : continuous_on g $ s ∩ closure tᶜ) :
+  continuous_on (piecewise t f g) s :=
+hf.if ht hg
+
+lemma continuous_if' {p : α → Prop} {f g : α → β} [∀ a, decidable (p a)]
+  (hpf : ∀ a ∈ frontier {x | p x}, tendsto f (𝓝[{x | p x}] a) (𝓝 $ ite (p a) (f a) (g a)))
+  (hpg : ∀ a ∈ frontier {x | p x}, tendsto g (𝓝[{x | ¬p x}] a) (𝓝 $ ite (p a) (f a) (g a)))
   (hf : continuous_on f {x | p x}) (hg : continuous_on g {x | ¬p x}) :
   continuous (λ a, ite (p a) (f a) (g a)) :=
 begin
   rw continuous_iff_continuous_on_univ,
-  apply continuous_on_if'; simp; assumption
+  apply continuous_on.if'; simp *; assumption
+end
+
+lemma continuous_if {p : α → Prop} {f g : α → β} [∀ a, decidable (p a)]
+  (hp : ∀ a ∈ frontier {x | p x}, f a = g a) (hf : continuous_on f (closure {x | p x}))
+  (hg : continuous_on g (closure {x | ¬p x})) :
+  continuous (λ a, if p a then f a else g a) :=
+begin
+  rw continuous_iff_continuous_on_univ,
+  apply continuous_on.if; simp; assumption
 end
 
+lemma continuous.if {p : α → Prop} {f g : α → β} [∀ a, decidable (p a)]
+  (hp : ∀ a ∈ frontier {x | p x}, f a = g a) (hf : continuous f) (hg : continuous g) :
+  continuous (λ a, if p a then f a else g a) :=
+continuous_if hp hf.continuous_on hg.continuous_on
+
+lemma continuous_piecewise {s : set α} {f g : α → β} [∀ a, decidable (a ∈ s)]
+  (hs : ∀ a ∈ frontier s, f a = g a) (hf : continuous_on f (closure s))
+  (hg : continuous_on g (closure sᶜ)) :
+  continuous (piecewise s f g) :=
+continuous_if hs hf hg
+
+lemma continuous.piecewise {s : set α} {f g : α → β} [∀ a, decidable (a ∈ s)]
+  (hs : ∀ a ∈ frontier s, f a = g a) (hf : continuous f) (hg : continuous g) :
+  continuous (piecewise s f g) :=
+hf.if hs hg
+
+lemma is_open_inter_union_inter_compl' {s s' t : set α}
+  (hs : is_open s) (hs' : is_open s') (ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s') :
+  is_open (s ∩ t ∪ s' ∩ tᶜ) :=
+begin
+  classical,
+  simp only [is_open_iff_continuous_mem] at *,
+  convert continuous_piecewise (λ x hx, propext (ht x hx)) hs.continuous_on hs'.continuous_on,
+  ext x, by_cases hx : x ∈ t; simp [hx]
+end
+
+lemma is_open_inter_union_inter_compl {s s' t : set α} (hs : is_open s) (hs' : is_open s')
+  (ht : s ∩ frontier t = s' ∩ frontier t) :
+  is_open (s ∩ t ∪ s' ∩ tᶜ) :=
+is_open_inter_union_inter_compl' hs hs' $ λ x hx, by simpa [hx] using ext_iff.1 ht x
+
 lemma continuous_on_fst {s : set (α × β)} : continuous_on prod.fst s :=
 continuous_fst.continuous_on
 

src/topology/order.lean

@@ -643,6 +643,9 @@ lemma continuous_Prop {p : α → Prop} : continuous p ↔ is_open {x | p x} :=
   continuous_generated_from $ assume s (hs : s ∈ {{true}}),
     by simp at hs; simp [hs, preimage, eq_true, h]⟩
 
+lemma is_open_iff_continuous_mem {s : set α} : is_open s ↔ continuous (λ x, x ∈ s) :=
+continuous_Prop.symm
+
 end sierpinski
 
 section infi

src/topology/path_connected.lean

@@ -225,11 +225,11 @@ path on `[0, 1/2]` and the second one on `[1/2, 1]`. -/
 { to_fun := (λ t : ℝ, if t ≤ 1/2 then γ.extend (2*t) else γ'.extend (2*t-1)) ∘ coe,
   continuous' :=
   begin
-    apply (continuous_if _ _ _).comp continuous_subtype_coe,
-    { norm_num },
+    refine (continuous.if_le _ _ continuous_id continuous_const (by norm_num)).comp
+      continuous_subtype_coe,
     -- TODO: the following are provable by `continuity` but it is too slow
-    { exact γ.continuous_extend.comp (continuous_const.mul continuous_id) },
-    { exact γ'.continuous_extend.comp ((continuous_const.mul continuous_id).sub continuous_const) }
+    exacts [γ.continuous_extend.comp (continuous_const.mul continuous_id),
+      γ'.continuous_extend.comp ((continuous_const.mul continuous_id).sub continuous_const)]
   end,
   source' := by norm_num,
   target' := by norm_num }
@@ -334,18 +334,15 @@ lemma trans_continuous_family {X ι : Type*} [topological_space X] [topological_
 begin
   have h₁' := path.continuous_uncurry_extend_of_continuous_family γ₁ h₁,
   have h₂' := path.continuous_uncurry_extend_of_continuous_family γ₂ h₂,
-  simp [has_uncurry.uncurry, has_coe_to_fun.coe, coe_fn, path.trans],
-  apply continuous_if _ _ _,
-  { rintros st hst,
-    have := frontier_le_subset_eq (continuous_subtype_coe.comp continuous_snd)
-      continuous_const hst,
-    simp only [mem_set_of_eq, comp_app] at this,
-    simp [this, mul_inv_cancel (@two_ne_zero ℝ _ _)] },
+  simp only [has_uncurry.uncurry, has_coe_to_fun.coe, coe_fn, path.trans, (∘)],
+  refine continuous.if_le _ _ (continuous_subtype_coe.comp continuous_snd) continuous_const _,
   { change continuous ((λ p : ι × ℝ, (γ₁ p.1).extend p.2) ∘ (prod.map id (λ x, 2*x : I → ℝ))),
     exact h₁'.comp (continuous_id.prod_map $ continuous_const.mul continuous_subtype_coe) },
   { change continuous ((λ p : ι × ℝ, (γ₂ p.1).extend p.2) ∘ (prod.map id (λ x, 2*x - 1 : I → ℝ))),
     exact h₂'.comp (continuous_id.prod_map $
       (continuous_const.mul continuous_subtype_coe).sub continuous_const) },
+  { rintros st hst,
+    simp [hst, mul_inv_cancel (@two_ne_zero ℝ _ _)] }
 end
 
 /-! #### Truncating a path -/