refactor(topology/continuous_on): move continuous_{on,within_at} to own file (#1516)

* refactor(topology/continuous_on): move continuous_{on,within_at} to own file

* Update src/topology/continuous_on.lean

Author: rwbarton

src/topology/algebra/monoid.lean

@@ -8,7 +8,7 @@ Theory of topological monoids.
 TODO: generalize `topological_monoid` and `topological_add_monoid` to semigroups, or add a type class
 `topological_operator α (*)`.
 -/
-import topology.constructions
+import topology.constructions topology.continuous_on
 import algebra.pi_instances
 
 open classical set lattice filter topological_space

src/topology/basic.lean

@@ -11,17 +11,14 @@ import order.filter
 
 The main definition is the type class `topological space α` which endows a type `α` with a topology.
 Then `set α` gets predicates `is_open`, `is_closed` and functions `interior`, `closure` and
-`frontier`. Each point `x` of `α` gets a neighborhood filter `nhds x`, and relative versions
-`nhds_within x s` for every set `s` in `α`.
+`frontier`. Each point `x` of `α` gets a neighborhood filter `nhds x`.
 
 This file also defines locally finite families of subsets of `α`.
 
 For topological spaces `α` and `β`, a function `f : α → β` and a point `a : α`,
 `continuous_at f a` means `f` is continuous at `a`, and global continuity is
-`continuous f`. There are also relative versions `continuous_within_at` and `continuous_on`
-and continuity `pcontinuous` for partially defined functions. Some basic properties
-of these various notions of continuity are proved in `topology.order`, after the
-ordering on topologies has been established.
+`continuous f`. There is also a version of continuity `pcontinuous` for
+partially defined functions.
 
 ## Implementation notes
 
@@ -549,129 +546,6 @@ noncomputable def lim (f : filter α) : α := epsilon $ λa, f ≤ nhds a
 lemma lim_spec {f : filter α} (h : ∃a, f ≤ nhds a) : f ≤ nhds (lim f) := epsilon_spec h
 end lim
 
-/-- The "neighborhood within" filter. Elements of `nhds_within a s` are sets containing the
-intersection of `s` and a neighborhood of `a`. -/
-def nhds_within (a : α) (s : set α) : filter α := nhds a ⊓ principal s
-
-theorem nhds_within_eq (a : α) (s : set α) :
-  nhds_within a s = ⨅ t ∈ {t : set α | a ∈ t ∧ is_open t}, principal (t ∩ s) :=
-have set.univ ∈ {s : set α | a ∈ s ∧ is_open s}, from ⟨set.mem_univ _, is_open_univ⟩,
-begin
-  rw [nhds_within, nhds, lattice.binfi_inf]; try { exact this },
-  simp only [inf_principal]
-end
-
-theorem nhds_within_univ (a : α) : nhds_within a set.univ = nhds a :=
-by rw [nhds_within, principal_univ, lattice.inf_top_eq]
-
-theorem mem_nhds_within (t : set α) (a : α) (s : set α) :
-  t ∈ nhds_within a s ↔ ∃ u, is_open u ∧ a ∈ u ∧ u ∩ s ⊆ t  :=
-begin
-  rw [nhds_within, mem_inf_principal, mem_nhds_sets_iff], split,
-  { rintros ⟨u, hu, openu, au⟩,
-    exact ⟨u, openu, au, λ x ⟨xu, xs⟩, hu xu xs⟩ },
-  rintros ⟨u, openu, au, hu⟩,
-  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_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_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 :=
-by rw [nhds_within_restrict t h₀ h₁, nhds_within_restrict u h₀ h₁, h₂]
-
-theorem nhds_within_eq_of_open {a : α} {s : set α} (h₀ : a ∈ s) (h₁ : is_open s) :
-  nhds_within a s = nhds a :=
-by rw [←nhds_within_univ]; apply nhds_within_eq_nhds_within h₀ h₁;
-     rw [set.univ_inter, set.inter_self]
-
-@[simp] theorem nhds_within_empty (a : α) : nhds_within a {} = ⊥ :=
-by rw [nhds_within, principal_empty, lattice.inf_bot_eq]
-
-theorem nhds_within_union (a : α) (s t : set α) :
-  nhds_within a (s ∪ t) = nhds_within a s ⊔ nhds_within a t :=
-by unfold nhds_within; rw [←lattice.inf_sup_left, sup_principal]
-
-theorem nhds_within_inter (a : α) (s t : set α) :
-  nhds_within a (s ∩ t) = nhds_within a s ⊓ nhds_within a t :=
-by unfold nhds_within; rw [lattice.inf_left_comm, lattice.inf_assoc, inf_principal,
-                             ←lattice.inf_assoc, lattice.inf_idem]
-
-theorem nhds_within_inter' (a : α) (s t : set α) :
-  nhds_within a (s ∩ t) = (nhds_within a s) ⊓ principal t :=
-by { unfold nhds_within, rw [←inf_principal, lattice.inf_assoc] }
-
-theorem tendsto_if_nhds_within {f g : α → β} {p : α → Prop} [decidable_pred p]
-    {a : α} {s : set α} {l : filter β}
-    (h₀ : tendsto f (nhds_within a (s ∩ p)) l)
-    (h₁ : tendsto g (nhds_within a (s ∩ {x | ¬ p x})) l) :
-  tendsto (λ x, if p x then f x else g x) (nhds_within a s) l :=
-by apply tendsto_if; rw [←nhds_within_inter']; assumption
-
-lemma map_nhds_within (f : α → β) (a : α) (s : set α) :
-  map f (nhds_within a s) =
-    ⨅ t ∈ {t : set α | a ∈ t ∧ is_open t}, principal (set.image f (t ∩ s)) :=
-have h₀ : directed_on ((λ (i : set α), principal (i ∩ s)) ⁻¹'o ge)
-        {x : set α | x ∈ {t : set α | a ∈ t ∧ is_open t}}, from
-  assume x ⟨ax, openx⟩ y ⟨ay, openy⟩,
-  ⟨x ∩ y, ⟨⟨ax, ay⟩, is_open_inter openx openy⟩,
-    le_principal_iff.mpr (set.inter_subset_inter_left _ (set.inter_subset_left _ _)),
-    le_principal_iff.mpr (set.inter_subset_inter_left _ (set.inter_subset_right _ _))⟩,
-have h₁ : ∃ (i : set α), i ∈ {t : set α | a ∈ t ∧ is_open t},
-  from ⟨set.univ, set.mem_univ _, is_open_univ⟩,
-by { rw [nhds_within_eq, map_binfi_eq h₀ h₁], simp only [map_principal] }
-
-theorem tendsto_nhds_within_mono_left {f : α → β} {a : α}
-    {s t : set α} {l : filter β} (hst : s ⊆ t) (h : tendsto f (nhds_within a t) l) :
-  tendsto f (nhds_within a s) l :=
-tendsto_le_left (nhds_within_mono a hst) h
-
-theorem tendsto_nhds_within_mono_right {f : β → α} {l : filter β}
-    {a : α} {s t : set α} (hst : s ⊆ t) (h : tendsto f l (nhds_within a s)) :
-  tendsto f l (nhds_within a t) :=
-tendsto_le_right (nhds_within_mono a hst) h
-
-theorem tendsto_nhds_within_of_tendsto_nhds {f : α → β} {a : α}
-    {s : set α} {l : filter β} (h : tendsto f (nhds a) l) :
-  tendsto f (nhds_within a s) l :=
-by rw [←nhds_within_univ] at h; exact tendsto_nhds_within_mono_left (set.subset_univ _) h
-
 
 /- locally finite family [General Topology (Bourbaki, 1995)] -/
 section locally_finite
@@ -731,14 +605,9 @@ def continuous (f : α → β) := ∀s, is_open s → is_open (f ⁻¹' s)
 if `f x` tends to `f x₀` when `x` tends to `x₀`. -/
 def continuous_at (f : α → β) (x : α) := tendsto f (nhds x) (nhds (f x))
 
-/-- A function between topological spaces is continuous at a point `x₀` within a subset `s`
-if `f x` tends to `f x₀` when `x` tends to `x₀` while staying within `s`. -/
-def continuous_within_at (f : α → β) (s : set α) (x : α) : Prop :=
-tendsto f (nhds_within x s) (nhds (f x))
-
-/-- A function between topological spaces is continuous on a subset `s`
-when it's continuous at every point of `s` within `s`. -/
-def continuous_on (f : α → β) (s : set α) : Prop := ∀ x ∈ s, continuous_within_at f s x
+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_id : continuous (id : α → α) :=
 assume s h, h
@@ -747,13 +616,22 @@ lemma continuous.comp {g : β → γ} {f : α → β} (hg : continuous g) (hf :
   continuous (g ∘ f) :=
 assume s h, hf _ (hg s h)
 
+lemma continuous_at.comp {g : β → γ} {f : α → β} {x : α}
+  (hg : continuous_at g (f x)) (hf : continuous_at f x) :
+  continuous_at (g ∘ f) x :=
+hg.comp hf
+
 lemma continuous.tendsto {f : α → β} (hf : continuous f) (x) :
   tendsto f (nhds x) (nhds (f x)) | s :=
 show s ∈ nhds (f x) → s ∈ map f (nhds x),
 by simp [nhds_sets]; exact
 assume t t_subset t_open fx_in_t,
   ⟨f ⁻¹' t, preimage_mono t_subset, hf t t_open, fx_in_t⟩
 
+lemma continuous.continuous_at {f : α → β} {x : α} (h : continuous f) :
+  continuous_at f x :=
+h.tendsto x
+
 lemma continuous_iff_continuous_at {f : α → β} : continuous f ↔ ∀ x, continuous_at f x :=
 ⟨continuous.tendsto,
   assume hf : ∀x, tendsto f (nhds x) (nhds (f x)),

src/topology/constructions.lean

@@ -54,19 +54,10 @@ lemma tendsto_prod_mk_nhds {γ} {a : α} {b : β} {f : filter γ} {ma : γ → 
   tendsto (λc, (ma c, mb c)) f (nhds (a, b)) :=
 by rw [nhds_prod_eq]; exact filter.tendsto.prod_mk ha hb
 
-lemma continuous_within_at.prod {f : α → β} {g : α → γ} {s : set α} {x : α}
-  (hf : continuous_within_at f s x) (hg : continuous_within_at g s x) :
-  continuous_within_at (λx, (f x, g x)) s x :=
-tendsto_prod_mk_nhds hf hg
-
 lemma continuous_at.prod {f : α → β} {g : α → γ} {x : α}
   (hf : continuous_at f x) (hg : continuous_at g x) : continuous_at (λx, (f x, g x)) x :=
 tendsto_prod_mk_nhds hf hg
 
-lemma continuous_on.prod {f : α → β} {g : α → γ} {s : set α}
-  (hf : continuous_on f s) (hg : continuous_on g s) : continuous_on (λx, (f x, g x)) s :=
-λx hx, continuous_within_at.prod (hf x hx) (hg x hx)
-
 lemma prod_generate_from_generate_from_eq {α : Type*} {β : Type*} {s : set (set α)} {t : set (set β)}
   (hs : ⋃₀ s = univ) (ht : ⋃₀ t = univ) :
   @prod.topological_space α β (generate_from s) (generate_from t) =