feat(topology/order): more facts on continuous_on (#1140)

Author: sgouezel

src/topology/algebra/group.lean

@@ -46,6 +46,11 @@ lemma continuous_inv [topological_group α] [topological_space β] {f : β → 
   (hf : continuous f) : continuous (λx, (f x)⁻¹) :=
 continuous_inv'.comp hf
 
+@[to_additive continuous_on.neg]
+lemma continuous_on.inv [topological_group α] [topological_space β] {f : β → α} {s : set β}
+  (hf : continuous_on f s) : continuous_on (λx, (f x)⁻¹) s :=
+continuous_inv'.comp_continuous_on hf
+
 @[to_additive tendsto_neg]
 lemma tendsto_inv [topological_group α] {f : β → α} {x : filter β} {a : α}
   (hf : tendsto f x (nhds a)) : tendsto (λx, (f x)⁻¹) x (nhds a⁻¹) :=
@@ -232,6 +237,10 @@ by simp; exact continuous_add hf (continuous_neg hg)
 lemma continuous_sub' [topological_add_group α] : continuous (λp:α×α, p.1 - p.2) :=
 continuous_sub continuous_fst continuous_snd
 
+lemma continuous_on.sub [topological_add_group α] [topological_space β] {f : β → α} {g : β → α} {s : set β}
+  (hf : continuous_on f s) (hg : continuous_on g s) : continuous_on (λx, f x - g x) s :=
+continuous_sub'.comp_continuous_on (hf.prod hg)
+
 lemma tendsto_sub [topological_add_group α] {f : β → α} {g : β → α} {x : filter β} {a b : α}
   (hf : tendsto f x (nhds a)) (hg : tendsto g x (nhds b)) : tendsto (λx, f x - g x) x (nhds (a - b)) :=
 by simp; exact tendsto_add hf (tendsto_neg hg)

src/topology/algebra/monoid.lean

@@ -54,6 +54,12 @@ continuous_mul continuous_const continuous_id
 lemma continuous_mul_right (a : α) : continuous (λ b:α, b * a) :=
 continuous_mul continuous_id continuous_const
 
+@[to_additive continuous_on.add]
+lemma continuous_on.mul [topological_space β] {f : β → α} {g : β → α} {s : set β}
+  (hf : continuous_on f s) (hg : continuous_on g s) :
+  continuous_on (λx, f x * g x) s :=
+(continuous_mul'.comp_continuous_on (hf.prod hg) : _)
+
 -- @[to_additive continuous_smul]
 lemma continuous_pow : ∀ n : ℕ, continuous (λ a : α, a ^ n)
 | 0 := by simpa using continuous_const

src/topology/basic.lean

@@ -545,23 +545,43 @@ begin
   exact ⟨u, λ x xu xs, hu ⟨xu, xs⟩, openu, au⟩
 end
 
+theorem self_mem_nhds_within {a : α} {s : set α} : s ∈ nhds_within a s :=
+begin
+  rw [nhds_within, mem_inf_principal],
+  simp only [imp_self],
+  exact univ_mem_sets
+end
+
 theorem inter_mem_nhds_within (s : set α) {t : set α} {a : α} (h : t ∈ nhds a) :
   s ∩ t ∈ nhds_within a s :=
 inter_mem_sets (mem_inf_sets_of_right (mem_principal_self s)) (mem_inf_sets_of_left h)
 
 theorem nhds_within_mono (a : α) {s t : set α} (h : s ⊆ t) : nhds_within a s ≤ nhds_within a t :=
 lattice.inf_le_inf (le_refl _) (principal_mono.mpr h)
 
-theorem nhds_within_restrict' {a : α} (s : set α) {t : set α} (h : t ∈ nhds a) :
+theorem nhds_within_restrict'' {a : α} (s : set α) {t : set α} (h : t ∈ nhds_within a s) :
   nhds_within a s = nhds_within a (s ∩ t) :=
 le_antisymm
-  (lattice.le_inf lattice.inf_le_left (le_principal_iff.mpr (inter_mem_nhds_within s h)))
+  (lattice.le_inf lattice.inf_le_left (le_principal_iff.mpr (inter_mem_sets self_mem_nhds_within h)))
   (lattice.inf_le_inf (le_refl _) (principal_mono.mpr (set.inter_subset_left _ _)))
 
+theorem nhds_within_restrict' {a : α} (s : set α) {t : set α} (h : t ∈ nhds a) :
+  nhds_within a s = nhds_within a (s ∩ t) :=
+nhds_within_restrict'' s $ mem_inf_sets_of_left h
+
 theorem nhds_within_restrict {a : α} (s : set α) {t : set α} (h₀ : a ∈ t) (h₁ : is_open t) :
   nhds_within a s = nhds_within a (s ∩ t) :=
 nhds_within_restrict' s (mem_nhds_sets h₁ h₀)
 
+theorem nhds_within_le_of_mem {a : α} {s t : set α} (h : s ∈ nhds_within a t) :
+  nhds_within a t ≤ nhds_within a s :=
+begin
+  rcases (mem_nhds_within _ _ _).1 h with ⟨u, u_open, au, uts⟩,
+  have : nhds_within a t = nhds_within a (t ∩ u) := nhds_within_restrict _ au u_open,
+  rw [this, inter_comm],
+  exact nhds_within_mono _ uts
+end
+
 theorem nhds_within_eq_nhds_within {a : α} {s t u : set α}
     (h₀ : a ∈ s) (h₁ : is_open s) (h₂ : t ∩ s = u ∩ s) :
   nhds_within a t = nhds_within a u :=

src/topology/order.lean

@@ -655,6 +655,16 @@ have ∀ t, is_open (function.restrict f s ⁻¹' t) ↔ ∃ (u : set α), is_op
   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,
+  begin
+    intro t,
+    rw [is_closed_induced_iff, function.restrict_eq, set.preimage_comp],
+    simp only [subtype.preimage_val_eq_preimage_val_iff]
+  end,
+by rw [continuous_on_iff_continuous_restrict, continuous_iff_is_closed]; simp only [this]
+
 theorem nhds_within_le_comap {x : α} {s : set α} {f : α → β} (ctsf : continuous_within_at f s x) :
   nhds_within x s ≤ comap f (nhds_within (f x) (f '' s)) :=
 map_le_iff_le_comap.1 ctsf.tendsto_nhds_within_image
@@ -671,6 +681,14 @@ lemma continuous_within_at.mono {f : α → β} {s t : set α} {x : α} (h : con
   (hs : s ⊆ t) : continuous_within_at f s x :=
 tendsto_le_left (nhds_within_mono x hs) h
 
+lemma continuous_within_at_inter' {f : α → β} {s t : set α} {x : α} (h : t ∈ nhds_within x s) :
+  continuous_within_at f (s ∩ t) x ↔ continuous_within_at f s x :=
+by simp [continuous_within_at, nhds_within_restrict'' s h]
+
+lemma continuous_within_at_inter {f : α → β} {s t : set α} {x : α} (h : t ∈ nhds x) :
+  continuous_within_at f (s ∩ t) x ↔ continuous_within_at f s x :=
+by simp [continuous_within_at, nhds_within_restrict' s h]
+
 lemma continuous_on.congr_mono {f g : α → β} {s s₁ : set α} (h : continuous_on f s)
   (h' : ∀x ∈ s₁, g x = f x) (h₁ : s₁ ⊆ s) : continuous_on g s₁ :=
 begin
@@ -690,6 +708,13 @@ lemma continuous_at.continuous_within_at {f : α → β} {s : set α} {x : α} (
   continuous_within_at f s x :=
 continuous_within_at.mono ((continuous_within_at_univ f x).2 h) (subset_univ _)
 
+lemma continuous_within_at.continuous_at {f : α → β} {s : set α} {x : α}
+  (h : continuous_within_at f s x) (hs : s ∈ nhds x) : continuous_at f x :=
+begin
+  have : s = univ ∩ s, by rw univ_inter,
+  rwa [this, continuous_within_at_inter hs, continuous_within_at_univ] at h
+end
+
 lemma continuous_within_at.comp {g : β → γ} {f : α → β} {s : set α} {t : set β} {x : α}
   (hg : continuous_within_at g t (f x)) (hf : continuous_within_at f s x) (h : f '' s ⊆ t) :
   continuous_within_at (g ∘ f) s x :=
@@ -727,15 +752,58 @@ begin
   exact h.mono (subset_univ _)
 end
 
+lemma continuous.comp_continuous_on {g : β → γ} {f : α → β} {s : set α}
+  (hg : continuous g) (hf : continuous_on f s) :
+  continuous_on (g ∘ f) s :=
+hg.continuous_on.comp hf (subset_univ _)
+
+lemma continuous.continuous_at {f : α → β} {x : α} (h : continuous f) :
+  continuous_at f x :=
+begin
+  have := continuous_iff_continuous_on_univ.1 h x (mem_univ _),
+  rwa continuous_within_at_univ at this,
+end
+
+lemma continuous_at.preimage_mem_nhds {f : α → β} {x : α} {t : set β} (h : continuous_at f x)
+  (ht : t ∈ nhds (f x)) : f ⁻¹' t ∈ nhds x :=
+h ht
+
+lemma continuous_within_at.preimage_mem_nhds_within {f : α → β} {x : α} {s : set α} {t : set β}
+  (h : continuous_within_at f s x) (ht : t ∈ nhds (f x)) : f ⁻¹' t ∈ nhds_within x s :=
+h ht
+
+lemma continuous_within_at.congr_of_mem_nhds_within {f f₁ : α → β} {s : set α} {x : α}
+  (h : continuous_within_at f s x) (h₁ : {y | f₁ y = f y} ∈ nhds_within x s) (hx : f₁ x = f x) :
+  continuous_within_at f₁ s x :=
+by rwa [continuous_within_at, filter.tendsto, hx, filter.map_cong h₁]
+
 lemma continuous_on_const {s : set α} {c : β} : continuous_on (λx, c) s :=
 continuous_const.continuous_on
 
+lemma continuous_on_open_iff {f : α → β} {s : set α} (hs : is_open s) :
+  continuous_on f s ↔ (∀t, _root_.is_open t → is_open (s ∩ f⁻¹' t)) :=
+begin
+  rw continuous_on_iff',
+  split,
+  { assume h t ht,
+    rcases h t ht with ⟨u, u_open, hu⟩,
+    rw [inter_comm, hu],
+    apply is_open_inter u_open hs },
+  { assume h t ht,
+    refine ⟨s ∩ f ⁻¹' t, h t ht, _⟩,
+    rw [@inter_comm _ s (f ⁻¹' t), inter_assoc, inter_self] }
+end
+
 lemma continuous_on.preimage_open_of_open {f : α → β} {s : set α} {t : set β}
   (hf : continuous_on f s) (hs : is_open s) (ht : is_open t) : is_open (s ∩ f⁻¹' t) :=
+(continuous_on_open_iff hs).1 hf t ht
+
+lemma continuous_on.preimage_closed_of_closed {f : α → β} {s : set α} {t : set β}
+  (hf : continuous_on f s) (hs : is_closed s) (ht : is_closed t) : is_closed (s ∩ f⁻¹' t) :=
 begin
-  rcases continuous_on_iff'.1 hf t ht with ⟨u, hu⟩,
+  rcases continuous_on_iff_is_closed.1 hf t ht with ⟨u, hu⟩,
   rw [inter_comm, hu.2],
-  apply is_open_inter hu.1 hs
+  apply is_closed_inter hu.1 hs
 end
 
 lemma continuous_on.preimage_interior_subset_interior_preimage {f : α → β} {s : set α} {t : set β}
@@ -757,6 +825,24 @@ begin
   rwa [continuous_within_at, ← nhds_within_restrict _ xt open_t] at this
 end
 
+lemma continuous_on_open_of_generate_from {β : Type*} {s : set α} {T : set (set β)} {f : α → β}
+  (hs : is_open s) (h : ∀t ∈ T, is_open (s ∩ f⁻¹' t)) :
+  @continuous_on α β _ (topological_space.generate_from T) f s :=
+begin
+  rw continuous_on_open_iff,
+  assume t ht,
+  induction ht with u hu u v Tu Tv hu hv U hU hU',
+  { exact h u hu },
+  { simp only [preimage_univ, inter_univ], exact hs },
+  { have : s ∩ f ⁻¹' (u ∩ v) = (s ∩ f ⁻¹' u) ∩ (s ∩ f ⁻¹' v),
+      by { ext x, simp, split, finish, finish },
+    rw this,
+    exact is_open_inter hu hv },
+  { rw [preimage_sUnion, inter_bUnion],
+    exact is_open_bUnion hU' },
+  { exact hs }
+end
+
 end topα
 
 end constructions