feat(topology/constructions): add map_fst_nhds and map_snd_nhds (#6142)

* Move the definition of `nhds_within` to `topology/basic`. The theory is still in `continuous_on`.
* Add `filter.map_inf_principal_preimage`.
* Add `map_fst_nhds_within`, `map_fst_nhds`, `map_snd_nhds_within`, and `map_snd_nhds`.

Author: urkud

src/order/filter/basic.lean

@@ -2206,6 +2206,10 @@ lemma tendsto_pure_left {f : α → β} {a : α} {l : filter β} :
   tendsto f (pure a) l ↔ ∀ s ∈ l, f a ∈ s :=
 iff.rfl
 
+@[simp] lemma map_inf_principal_preimage {f : α → β} {s : set β} {l : filter α} :
+  map f (l ⊓ 𝓟 (f ⁻¹' s)) = map f l ⊓ 𝓟 s :=
+filter.ext $ λ t, by simp only [mem_map, mem_inf_principal, mem_set_of_eq, mem_preimage]
+
 /-- If two filters are disjoint, then a function cannot tend to both of them along a non-trivial
 filter. -/
 lemma tendsto.not_tendsto {f : α → β} {a : filter α} {b₁ b₂ : filter β} (hf : tendsto f a b₁)

src/topology/basic.lean

@@ -29,6 +29,7 @@ partially defined functions.
 
 * `𝓝 x`: the filter of neighborhoods of a point `x`;
 * `𝓟 s`: the principal filter of a set `s`;
+* `𝓝[s] x`: the filter `nhds_within x s` of neighborhoods of a point `x` within a set `s`.
 
 ## Implementation notes
 
@@ -480,6 +481,12 @@ infimum over the principal filters of all open sets containing `a`. -/
 
 localized "notation `𝓝` := nhds" in topological_space
 
+/-- The "neighborhood within" filter. Elements of `𝓝[s] a` are sets containing the
+intersection of `s` and a neighborhood of `a`. -/
+def nhds_within (a : α) (s : set α) : filter α := 𝓝 a ⊓ 𝓟 s
+
+localized "notation `𝓝[` s `] ` x:100 := nhds_within x s" in topological_space
+
 lemma nhds_def (a : α) : 𝓝 a = (⨅ s ∈ {s : set α | a ∈ s ∧ is_open s}, 𝓟 s) := by rw nhds
 
 /-- The open sets containing `a` are a basis for the neighborhood filter. See `nhds_basis_opens'`

src/topology/constructions.lean

@@ -269,28 +269,43 @@ lemma exists_nhds_square {s : set (α × α)} {x : α} (hx : s ∈ 𝓝 (x, x))
   ∃U, is_open U ∧ x ∈ U ∧ set.prod U U ⊆ s :=
 by simpa [nhds_prod_eq, (nhds_basis_opens x).prod_self.mem_iff, and.assoc, and.left_comm] using hx
 
+/-- `prod.fst` maps neighborhood of `x : α × β` within the section `prod.snd ⁻¹' {x.2}`
+to `𝓝 x.1`. -/
+lemma map_fst_nhds_within (x : α × β) : map prod.fst (𝓝[prod.snd ⁻¹' {x.2}] x) = 𝓝 x.1 :=
+begin
+  refine le_antisymm (continuous_at_fst.mono_left inf_le_left) (λ s hs, _),
+  rcases x with ⟨x, y⟩,
+  rw [mem_map, nhds_within, mem_inf_principal, mem_nhds_prod_iff] at hs,
+  rcases hs with ⟨u, hu, v, hv, H⟩,
+  simp only [prod_subset_iff, mem_singleton_iff, mem_set_of_eq, mem_preimage] at H,
+  exact mem_sets_of_superset hu (λ z hz, H _ hz _ (mem_of_nhds hv) rfl)
+end
+
+@[simp] lemma map_fst_nhds (x : α × β) : map prod.fst (𝓝 x) = 𝓝 x.1 :=
+le_antisymm continuous_at_fst $ (map_fst_nhds_within x).symm.trans_le (map_mono inf_le_left)
+
 /-- The first projection in a product of topological spaces sends open sets to open sets. -/
 lemma is_open_map_fst : is_open_map (@prod.fst α β) :=
+is_open_map_iff_nhds_le.2 $ λ x, (map_fst_nhds x).ge
+
+/-- `prod.snd` maps neighborhood of `x : α × β` within the section `prod.fst ⁻¹' {x.1}`
+to `𝓝 x.2`. -/
+lemma map_snd_nhds_within (x : α × β) : map prod.snd (𝓝[prod.fst ⁻¹' {x.1}] x) = 𝓝 x.2 :=
 begin
-  rw is_open_map_iff_nhds_le,
-  rintro ⟨x, y⟩ s hs,
-  rcases mem_nhds_prod_iff.1 hs with ⟨tx, htx, ty, hty, ht⟩,
-  simp only [subset_def, prod.forall, mem_prod] at ht,
-  exact mem_sets_of_superset htx (λ x hx, ht x y ⟨hx, mem_of_nhds hty⟩)
+  refine le_antisymm (continuous_at_snd.mono_left inf_le_left) (λ s hs, _),
+  rcases x with ⟨x, y⟩,
+  rw [mem_map, nhds_within, mem_inf_principal, mem_nhds_prod_iff] at hs,
+  rcases hs with ⟨u, hu, v, hv, H⟩,
+  simp only [prod_subset_iff, mem_singleton_iff, mem_set_of_eq, mem_preimage] at H,
+  exact mem_sets_of_superset hv (λ z hz, H _ (mem_of_nhds hu) _ hz rfl)
 end
 
+@[simp] lemma map_snd_nhds (x : α × β) : map prod.snd (𝓝 x) = 𝓝 x.2 :=
+le_antisymm continuous_at_snd $ (map_snd_nhds_within x).symm.trans_le (map_mono inf_le_left)
+
 /-- The second projection in a product of topological spaces sends open sets to open sets. -/
 lemma is_open_map_snd : is_open_map (@prod.snd α β) :=
-begin
-  /- This lemma could be proved by composing the fact that the first projection is open, and
-  exchanging coordinates is a homeomorphism, hence open. As the `prod_comm` homeomorphism is defined
-  later, we rather go for the direct proof, copy-pasting the proof for the first projection. -/
-  rw is_open_map_iff_nhds_le,
-  rintro ⟨x, y⟩ s hs,
-  rcases mem_nhds_prod_iff.1 hs with ⟨tx, htx, ty, hty, ht⟩,
-  simp only [subset_def, prod.forall, mem_prod] at ht,
-  exact mem_sets_of_superset hty (λ y hy, ht x y ⟨mem_of_nhds htx, hy⟩)
-end
+is_open_map_iff_nhds_le.2 $ λ x, (map_snd_nhds x).ge
 
 /-- A product set is open in a product space if and only if each factor is open, or one of them is
 empty -/

src/topology/continuous_on.lean

@@ -32,12 +32,6 @@ open_locale topological_space filter
 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
 variables [topological_space α]
 
-/-- The "neighborhood within" filter. Elements of `𝓝[s] a` are sets containing the
-intersection of `s` and a neighborhood of `a`. -/
-def nhds_within (a : α) (s : set α) : filter α := 𝓝 a ⊓ 𝓟 s
-
-localized "notation `𝓝[` s `] ` x:100 := nhds_within x s" in topological_space
-
 @[simp] lemma nhds_bind_nhds_within {a : α} {s : set α} :
   (𝓝 a).bind (λ x, 𝓝[s] x) = 𝓝[s] a :=
 bind_inf_principal.trans $ congr_arg2 _ nhds_bind_nhds rfl