feat(order/topology/filter): define topology on filter X (#17219)

src/data/set/basic.lean

@@ -2167,6 +2167,15 @@ lemma subset_range_iff_exists_image_eq {f : α → β} {s : set β} :
   s ⊆ range f ↔ ∃ t, f '' t = s :=
 ⟨λ h, ⟨_, image_preimage_eq_iff.2 h⟩, λ ⟨t, ht⟩, ht ▸ image_subset_range _ _⟩
 
+@[simp] lemma exists_subset_range_and_iff {f : α → β} {p : set β → Prop} :
+  (∃ s, s ⊆ range f ∧ p s) ↔ ∃ s, p (f '' s) :=
+⟨λ ⟨s, hsf, hps⟩, ⟨f ⁻¹' s, (image_preimage_eq_of_subset hsf).symm ▸ hps⟩,
+  λ ⟨s, hs⟩, ⟨f '' s, image_subset_range _ _, hs⟩⟩
+
+lemma exists_subset_range_iff {f : α → β} {p : set β → Prop} :
+  (∃ s ⊆ range f, p s) ↔ ∃ s, p (f '' s) :=
+by simp only [exists_prop, exists_subset_range_and_iff]
+
 lemma range_image (f : α → β) : range (image f) = 𝒫 (range f) :=
 ext $ λ s, subset_range_iff_exists_image_eq.symm
 

src/topology/algebra/order/filter.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import topology.algebra.order.basic
+import topology.filter
+
+/-!
+# Topology on filters of a space with order topology
+
+In this file we prove that `𝓝 (f x)` tends to `𝓝 filter.at_top` provided that `f` tends to
+`filter.at_top`, and similarly for `filter.at_bot`.
+-/
+
+open_locale topological_space
+
+namespace filter
+
+variables {α X : Type*} [topological_space X] [partial_order X] [order_topology X]
+
+protected lemma tendsto_nhds_at_top [no_max_order X] : tendsto 𝓝 (at_top : filter X) (𝓝 at_top) :=
+filter.tendsto_nhds_at_top_iff.2 $ λ x, (eventually_gt_at_top x).mono $ λ y, le_mem_nhds
+
+protected lemma tendsto_nhds_at_bot [no_min_order X] : tendsto 𝓝 (at_bot : filter X) (𝓝 at_bot) :=
+@filter.tendsto_nhds_at_top Xᵒᵈ _ _ _ _
+
+lemma tendsto.nhds_at_top [no_max_order X] {f : α → X} {l : filter α} (h : tendsto f l at_top) :
+  tendsto (𝓝 ∘ f) l (𝓝 at_top) :=
+filter.tendsto_nhds_at_top.comp h
+
+lemma tendsto.nhds_at_bot [no_min_order X] {f : α → X} {l : filter α} (h : tendsto f l at_bot) :
+  tendsto (𝓝 ∘ f) l (𝓝 at_bot) :=
+@tendsto.nhds_at_top α Xᵒᵈ _ _ _ _ _ _ h
+
+end filter

src/topology/bases.lean

@@ -173,6 +173,11 @@ lemma is_topological_basis.open_eq_sUnion {B : set (set α)}
   ∃ S ⊆ B, u = ⋃₀ S :=
 ⟨{s ∈ B | s ⊆ u}, λ s h, h.1, hB.open_eq_sUnion' ou⟩
 
+lemma is_topological_basis.open_iff_eq_sUnion {B : set (set α)}
+  (hB : is_topological_basis B) {u : set α} :
+  is_open u ↔ ∃ S ⊆ B, u = ⋃₀ S :=
+⟨hB.open_eq_sUnion, λ ⟨S, hSB, hu⟩, hu.symm ▸ is_open_sUnion (λ s hs, hB.is_open (hSB hs))⟩
+
 lemma is_topological_basis.open_eq_Union {B : set (set α)}
   (hB : is_topological_basis B) {u : set α} (ou : is_open u) :
   ∃ (β : Type u) (f : β → set α), u = (⋃ i, f i) ∧ ∀ i, f i ∈ B :=

src/topology/filter.lean

@@ -0,0 +1,188 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import order.filter.lift
+import topology.separation
+import data.set.intervals.monotone
+
+/-!
+# Topology on the set of filters on a type
+
+In this file introduce topology on `filter α`. It is generated by the sets
+`set.Iic (𝓟 s) = {l : filter α | s ∈ l}`, `s : set α`. A set `s : set (filter α)` is open if and
+only if it is a union of a family of these basic open sets, see `filter.is_open_iff`.
+
+This topology has the following important properties.
+
+* If `X` is a topological space, then the map `𝓝 : X → filter X` is a topology inducing map.
+
+* In particular, it is a continuous map, so `𝓝 ∘ f` tends to `𝓝 (𝓝 a)` whenever `f` tends to `𝓝 a`.
+
+* If `X` is an ordered topological space with order topology and no max element, then `𝓝 ∘ f` tends
+  to `𝓝 filter.at_top` whenever `f` tends to `filter.at_top`.
+
+* It turns `filter X` into a T₀ space and the order on `filter X` is the dual of the
+  `specialization_order (filter X)`.
+
+## Tags
+
+filter, topological space
+-/
+
+open set filter topological_space
+open_locale filter topological_space
+
+variables {ι : Sort*} {α β X Y : Type*}
+
+namespace filter
+
+/-- Topology on `filter α` is generated by the sets `set.Iic (𝓟 s) = {l : filter α | s ∈ l}`,
+`s : set α`. A set `s : set (filter α)` is open if and only if it is a union of a family of these
+basic open sets, see `filter.is_open_iff`. -/
+instance : topological_space (filter α) := generate_from $ range $ Iic ∘ 𝓟
+
+lemma is_open_Iic_principal {s : set α} : is_open (Iic (𝓟 s)) :=
+generate_open.basic _ (mem_range_self _)
+
+lemma is_open_set_of_mem {s : set α} : is_open {l : filter α | s ∈ l} :=
+by simpa only [Iic_principal] using is_open_Iic_principal
+
+lemma is_topological_basis_Iic_principal :
+  is_topological_basis (range (Iic ∘ 𝓟 : set α → set (filter α))) :=
+{ exists_subset_inter :=
+    begin
+      rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩ l hl,
+      exact ⟨Iic (𝓟 s) ∩ Iic (𝓟 t), ⟨s ∩ t, by simp⟩, hl, subset.rfl⟩
+    end,
+  sUnion_eq := sUnion_eq_univ_iff.2 $ λ l, ⟨Iic ⊤, ⟨univ, congr_arg Iic principal_univ⟩, le_top⟩,
+  eq_generate_from := rfl }
+
+lemma is_open_iff {s : set (filter α)} :
+  is_open s ↔ ∃ T : set (set α), s = ⋃ t ∈ T, Iic (𝓟 t) :=
+is_topological_basis_Iic_principal.open_iff_eq_sUnion.trans $
+  by simp only [exists_subset_range_iff, sUnion_image]
+
+lemma nhds_eq (l : filter α) : 𝓝 l = l.lift' (Iic ∘ 𝓟) :=
+nhds_generate_from.trans $ by simp only [mem_set_of_eq, and_comm (l ∈ _), infi_and, infi_range,
+  filter.lift', filter.lift, (∘), mem_Iic, le_principal_iff]
+
+lemma nhds_eq' (l : filter α) : 𝓝 l = l.lift' (λ s, {l' | s ∈ l'}) :=
+by simpa only [(∘), Iic_principal] using nhds_eq l
+
+protected lemma tendsto_nhds {la : filter α} {lb : filter β} {f : α → filter β} :
+  tendsto f la (𝓝 lb) ↔ ∀ s ∈ lb, ∀ᶠ a in la, s ∈ f a :=
+by simp only [nhds_eq', tendsto_lift', mem_set_of_eq]
+
+lemma has_basis.nhds {l : filter α} {p : ι → Prop} {s : ι → set α} (h : has_basis l p s) :
+  has_basis (𝓝 l) p (λ i, Iic (𝓟 (s i))) :=
+by { rw nhds_eq, exact h.lift' monotone_principal.Iic }
+
+/-- Neighborhoods of a countably generated filter is a countably generated filter. -/
+instance {l : filter α} [is_countably_generated l] : is_countably_generated (𝓝 l) :=
+let ⟨b, hb⟩ := l.exists_antitone_basis in has_countable_basis.is_countably_generated $
+  ⟨hb.nhds, set.to_countable _⟩
+
+lemma has_basis.nhds' {l : filter α} {p : ι → Prop} {s : ι → set α} (h : has_basis l p s) :
+  has_basis (𝓝 l) p (λ i, {l' | s i ∈ l'}) :=
+by simpa only [Iic_principal] using h.nhds
+
+lemma mem_nhds_iff {l : filter α} {S : set (filter α)} :
+  S ∈ 𝓝 l ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ S :=
+l.basis_sets.nhds.mem_iff
+
+lemma mem_nhds_iff' {l : filter α} {S : set (filter α)} :
+  S ∈ 𝓝 l ↔ ∃ t ∈ l, ∀ ⦃l' : filter α⦄, t ∈ l' → l' ∈ S :=
+l.basis_sets.nhds'.mem_iff
+
+@[simp] lemma nhds_bot : 𝓝 (⊥ : filter α) = pure ⊥ :=
+by simp [nhds_eq, lift'_bot monotone_principal.Iic]
+
+@[simp] lemma nhds_top : 𝓝 (⊤ : filter α) = ⊤ := by simp [nhds_eq]
+
+@[simp] lemma nhds_principal (s : set α) : 𝓝 (𝓟 s) = 𝓟 (Iic (𝓟 s)) :=
+(has_basis_principal s).nhds.eq_of_same_basis (has_basis_principal _)
+
+@[simp] lemma nhds_pure (x : α) : 𝓝 (pure x : filter α) = 𝓟 {⊥, pure x} :=
+by rw [← principal_singleton, nhds_principal, principal_singleton, Iic_pure]
+
+@[simp] lemma nhds_infi (f : ι → filter α) : 𝓝 (⨅ i, f i) = ⨅ i, 𝓝 (f i) :=
+by { simp only [nhds_eq], apply lift'_infi_of_map_univ; simp }
+
+@[simp] lemma nhds_inf (l₁ l₂ : filter α) : 𝓝 (l₁ ⊓ l₂) = 𝓝 l₁ ⊓ 𝓝 l₂ :=
+by simpa only [infi_bool_eq] using nhds_infi (λ b, cond b l₁ l₂)
+
+lemma monotone_nhds : monotone (𝓝 : filter α → filter (filter α)) :=
+monotone.of_map_inf nhds_inf
+
+lemma Inter_nhds (l : filter α) : ⋂₀ {s | s ∈ 𝓝 l} = Iic l :=
+by simp only [nhds_eq, sInter_lift'_sets monotone_principal.Iic, Iic, le_principal_iff,
+  ← set_of_forall, ← filter.le_def]
+
+@[simp] lemma nhds_mono {l₁ l₂ : filter α} : 𝓝 l₁ ≤ 𝓝 l₂ ↔ l₁ ≤ l₂ :=
+begin
+  refine ⟨λ h, _, λ h, monotone_nhds h⟩,
+  rw [← Iic_subset_Iic, ← Inter_nhds, ← Inter_nhds],
+  exact sInter_subset_sInter h
+end
+
+protected lemma mem_interior {s : set (filter α)} {l : filter α} :
+  l ∈ interior s ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s :=
+by rw [mem_interior_iff_mem_nhds, mem_nhds_iff]
+
+protected lemma mem_closure {s : set (filter α)} {l : filter α} :
+  l ∈ closure s ↔ ∀ t ∈ l, ∃ l' ∈ s, t ∈ l' :=
+by simp only [closure_eq_compl_interior_compl, filter.mem_interior, mem_compl_iff, not_exists,
+  not_forall, not_not, exists_prop, not_and, and_comm, subset_def, mem_Iic, le_principal_iff]
+
+@[simp] protected lemma closure_singleton (l : filter α) : closure {l} = Ici l :=
+by { ext l', simp [filter.mem_closure, filter.le_def] }
+
+@[simp] lemma specializes_iff_le {l₁ l₂ : filter α} : l₁ ⤳ l₂ ↔ l₁ ≤ l₂ :=
+by simp only [specializes_iff_closure_subset, filter.closure_singleton, Ici_subset_Ici]
+
+instance : t0_space (filter α) :=
+⟨λ x y h, (specializes_iff_le.1 h.specializes).antisymm (specializes_iff_le.1 h.symm.specializes)⟩
+
+lemma nhds_at_top [preorder α] : 𝓝 at_top = ⨅ x : α, 𝓟 (Iic (𝓟 (Ici x))) :=
+by simp only [at_top, nhds_infi, nhds_principal]
+
+protected lemma tendsto_nhds_at_top_iff [preorder β] {l : filter α} {f : α → filter β} :
+  tendsto f l (𝓝 at_top) ↔ ∀ y, ∀ᶠ a in l, Ici y ∈ f a :=
+by simp only [nhds_at_top, tendsto_infi, tendsto_principal, mem_Iic, le_principal_iff]
+
+lemma nhds_at_bot [preorder α] : 𝓝 at_bot = ⨅ x : α, 𝓟 (Iic (𝓟 (Iic x))) := @nhds_at_top αᵒᵈ _
+
+protected lemma tendsto_nhds_at_bot_iff [preorder β] {l : filter α} {f : α → filter β} :
+  tendsto f l (𝓝 at_bot) ↔ ∀ y, ∀ᶠ a in l, Iic y ∈ f a :=
+@filter.tendsto_nhds_at_top_iff α βᵒᵈ _ _ _
+
+variables [topological_space X]
+
+lemma nhds_nhds (x : X) :
+  𝓝 (𝓝 x) = ⨅ (s : set X) (hs : is_open s) (hx : x ∈ s), 𝓟 (Iic (𝓟 s)) :=
+by simp only [(nhds_basis_opens x).nhds.eq_binfi, infi_and, @infi_comm _ (_ ∈ _)]
+
+lemma inducing_nhds : inducing (𝓝 : X → filter X) :=
+inducing_iff_nhds.2 $ λ x, (nhds_def' _).trans $
+  by simp only [nhds_nhds, comap_infi, comap_principal, Iic_principal, preimage_set_of_eq,
+    ← mem_interior_iff_mem_nhds, set_of_mem_eq, is_open.interior_eq] { contextual := tt }
+
+@[continuity] lemma continuous_nhds : continuous (𝓝 : X → filter X) := inducing_nhds.continuous
+
+protected lemma tendsto.nhds {f : α → X} {l : filter α} {x : X} (h : tendsto f l (𝓝 x)) :
+  tendsto (𝓝 ∘ f) l (𝓝 (𝓝 x)) :=
+(continuous_nhds.tendsto _).comp h
+
+end filter
+
+variables [topological_space X] [topological_space Y] {f : X → Y} {x : X} {s : set X}
+
+lemma continuous_within_at.nhds (h : continuous_within_at f s x) :
+  continuous_within_at (𝓝 ∘ f) s x :=
+h.nhds
+
+lemma continuous_at.nhds (h : continuous_at f x) : continuous_at (𝓝 ∘ f) x := h.nhds
+lemma continuous_on.nhds (h : continuous_on f s) : continuous_on (𝓝 ∘ f) s := λ x hx, (h x hx).nhds
+lemma continuous.nhds (h : continuous f) : continuous (𝓝 ∘ f) := filter.continuous_nhds.comp h