Mathlib.Topology.Filter

Filter.instTopologicalSpace instance

: TopologicalSpace (Filter α)

Full source

/-- The 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.isOpen_iff`. -/
instance : TopologicalSpace (Filter α) :=
  generateFrom <| range <| IicIic ∘ 𝓟

The Topological Space Structure on Filters

Informal description

The set of filters $\text{Filter } \alpha$ on a type $\alpha$ is equipped with a topology generated by the basic open sets $\{l : \text{Filter } \alpha \mid s \in l\}$ for each subset $s \subseteq \alpha$. A subset of $\text{Filter } \alpha$ is open if and only if it is a union of such basic open sets.

Filter.isOpen_Iic_principal theorem

{s : Set α} : IsOpen (Iic (𝓟 s))

Full source

theorem isOpen_Iic_principal {s : Set α} : IsOpen (Iic (𝓟 s)) :=
  GenerateOpen.basic _ (mem_range_self _)

Openness of Principal Filter Sets in Filter Topology

Informal description

For any subset $s$ of a type $\alpha$, the set $\{l : \text{Filter } \alpha \mid s \in l\}$ is open in the topology on $\text{Filter } \alpha$.

Filter.isOpen_setOf_mem theorem

{s : Set α} : IsOpen {l : Filter α | s ∈ l}

Full source

theorem isOpen_setOf_mem {s : Set α} : IsOpen { l : Filter α | s ∈ l } := by
  simpa only [Iic_principal] using isOpen_Iic_principal

Openness of the Set of Filters Containing a Given Subset

Informal description

For any subset $s$ of a type $\alpha$, the set $\{l \in \text{Filter } \alpha \mid s \in l\}$ is open in the topology on $\text{Filter } \alpha$.

Filter.isTopologicalBasis_Iic_principal theorem

: IsTopologicalBasis (range (Iic ∘ 𝓟 : Set α → Set (Filter α)))

Full source

theorem isTopologicalBasis_Iic_principal :
    IsTopologicalBasis (range (IicIic ∘ 𝓟 : Set α → Set (Filter α))) :=
  { exists_subset_inter := by
      rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩ l hl
      exact ⟨Iic (𝓟 s) ∩ Iic (𝓟 t), ⟨s ∩ t, by simp⟩, hl, Subset.rfl⟩
    sUnion_eq := sUnion_eq_univ_iff.2 fun _ => ⟨Iic ⊤, ⟨univ, congr_arg Iic principal_univ⟩,
      mem_Iic.2 le_top⟩
    eq_generateFrom := rfl }

Principal Filter Sets Form a Topological Basis

Informal description

The collection of all sets of the form $\{l : \text{Filter } \alpha \mid s \in l\}$ for subsets $s \subseteq \alpha$ forms a topological basis for the topology on $\text{Filter } \alpha$.

Filter.isOpen_iff theorem

{s : Set (Filter α)} : IsOpen s ↔ ∃ T : Set (Set α), s = ⋃ t ∈ T, Iic (𝓟 t)

Full source

theorem isOpen_iff {s : Set (Filter α)} : IsOpenIsOpen s ↔ ∃ T : Set (Set α), s = ⋃ t ∈ T, Iic (𝓟 t) :=
  isTopologicalBasis_Iic_principal.open_iff_eq_sUnion.trans <| by
    simp only [exists_subset_range_and_iff, sUnion_image, (· ∘ ·)]

Characterization of Open Sets in the Space of Filters

Informal description

A subset $s$ of the space of filters on a type $\alpha$ is open if and only if there exists a collection $T$ of subsets of $\alpha$ such that $s$ can be expressed as the union of all sets of the form $\{l \in \text{Filter } \alpha \mid t \in l\}$ for $t \in T$.

Filter.nhds_eq theorem

(l : Filter α) : 𝓝 l = l.lift' (Iic ∘ 𝓟)

Full source

theorem nhds_eq (l : Filter α) : 𝓝 l = l.lift' (IicIic ∘ 𝓟) :=
  nhds_generateFrom.trans <| by
    simp only [mem_setOf_eq, @and_comm (l ∈ _), iInf_and, iInf_range, Filter.lift', Filter.lift,
      (· ∘ ·), mem_Iic, le_principal_iff]

Neighborhood Filter Characterization in Filter Topology

Informal description

For any filter $l$ on a type $\alpha$, the neighborhood filter $\mathcal{N}(l)$ in the topology on $\text{Filter } \alpha$ is equal to the lift of the function that maps each subset $s \subseteq \alpha$ to the left-infinite right-closed interval $\{l' \in \text{Filter } \alpha \mid s \in l'\}$.

Filter.nhds_eq' theorem

(l : Filter α) : 𝓝 l = l.lift' fun s => {l' | s ∈ l'}

Full source

theorem nhds_eq' (l : Filter α) : 𝓝 l = l.lift' fun s => { l' | s ∈ l' } := by
  simpa only [Function.comp_def, Iic_principal] using nhds_eq l

Neighborhood Filter Characterization via Set Membership in Filter Topology

Informal description

For any filter $l$ on a type $\alpha$, the neighborhood filter $\mathcal{N}(l)$ in the topology on $\text{Filter } \alpha$ is equal to the lift of the function that maps each subset $s \subseteq \alpha$ to the set $\{l' \in \text{Filter } \alpha \mid s \in l'\}$.

Filter.tendsto_nhds theorem

 {la : Filter α} {lb : Filter β} {f : α → Filter β} : Tendsto f la (𝓝 lb) ↔ ∀ s ∈ lb, ∀ᶠ a in la, s ∈ f a

Full source

protected theorem tendsto_nhds {la : Filter α} {lb : Filter β} {f : α → Filter β} :
    TendstoTendsto f la (𝓝 lb) ↔ ∀ s ∈ lb, ∀ᶠ a in la, s ∈ f a := by
  simp only [nhds_eq', tendsto_lift', mem_setOf_eq]

Characterization of Filter Convergence in Filter Topology

Informal description

Let $f : \alpha \to \text{Filter } \beta$ be a function between types $\alpha$ and $\beta$, and let $l_a$ and $l_b$ be filters on $\alpha$ and $\beta$ respectively. The function $f$ tends to the neighborhood filter $\mathcal{N}(l_b)$ with respect to $l_a$ if and only if for every set $s$ in $l_b$, the set $\{a \in \alpha \mid s \in f(a)\}$ is eventually in $l_a$.

Filter.HasBasis.nhds theorem

 {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : HasBasis l p s) : HasBasis (𝓝 l) p fun i => Iic (𝓟 (s i))

Full source

protected theorem HasBasis.nhds {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : HasBasis l p s) :
    HasBasis (𝓝 l) p fun i => Iic (𝓟 (s i)) := by
  rw [nhds_eq]
  exact h.lift' monotone_principal.Iic

Neighborhood Filter Basis Characterization in Filter Topology

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis $\{s_i\}_{i \in \iota}$ indexed by a type $\iota$ and a predicate $p : \iota \to \text{Prop}$. Then the neighborhood filter $\mathcal{N}(l)$ in the topology on $\text{Filter } \alpha$ has a basis consisting of the sets $\{l' \in \text{Filter } \alpha \mid s_i \in l'\}$ for each $i \in \iota$ satisfying $p(i)$.

Filter.tendsto_pure_self theorem

(l : Filter X) : Tendsto (pure : X → Filter X) l (𝓝 l)

Full source

protected theorem tendsto_pure_self (l : Filter X) :
    Tendsto (pure : X → Filter X) l (𝓝 l) := by
  rw [Filter.tendsto_nhds]
  exact fun s hs ↦ Eventually.mono hs fun x ↦ id

Continuity of the Pure Filter Map in the Filter Topology

Informal description

For any filter $l$ on a type $X$, the function $\text{pure} : X \to \text{Filter } X$ tends to the neighborhood filter $\mathcal{N}(l)$ with respect to $l$ itself. In other words, the map sending each point $x \in X$ to its principal filter $\text{pure } x$ is continuous at $l$ in the topology on $\text{Filter } X$.

Filter.instIsCountablyGeneratedNhds instance

{l : Filter α} [IsCountablyGenerated l] : IsCountablyGenerated (𝓝 l)

Full source

/-- Neighborhoods of a countably generated filter is a countably generated filter. -/
instance {l : Filter α} [IsCountablyGenerated l] : IsCountablyGenerated (𝓝 l) :=
  let ⟨_b, hb⟩ := l.exists_antitone_basis
  HasCountableBasis.isCountablyGenerated <| ⟨hb.nhds, Set.to_countable _⟩

Countable Generation of Neighborhood Filters in Filter Topology

Informal description

For any countably generated filter $l$ on a type $\alpha$, the neighborhood filter $\mathcal{N}(l)$ in the topology on $\text{Filter } \alpha$ is also countably generated.

Filter.HasBasis.nhds' theorem

 {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : HasBasis l p s) : HasBasis (𝓝 l) p fun i => {l' | s i ∈ l'}

Full source

theorem HasBasis.nhds' {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : HasBasis l p s) :
    HasBasis (𝓝 l) p fun i => { l' | s i ∈ l' } := by simpa only [Iic_principal] using h.nhds

Basis Characterization of Neighborhood Filters in Filter Topology

Informal description

Let $l$ be a filter on a type $\alpha$ with a basis $\{s_i\}_{i \in \iota}$ indexed by a type $\iota$ and a predicate $p : \iota \to \text{Prop}$. Then the neighborhood filter $\mathcal{N}(l)$ in the topology on $\text{Filter } \alpha$ has a basis consisting of the sets $\{l' \in \text{Filter } \alpha \mid s_i \in l'\}$ for each $i \in \iota$ satisfying $p(i)$.

Filter.mem_nhds_iff theorem

{l : Filter α} {S : Set (Filter α)} : S ∈ 𝓝 l ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ S

Full source

protected theorem mem_nhds_iff {l : Filter α} {S : Set (Filter α)} :
    S ∈ 𝓝 lS ∈ 𝓝 l ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ S :=
  l.basis_sets.nhds.mem_iff

Neighborhood Characterization in Filter Topology: $S \in \mathcal{N}(l) \leftrightarrow \exists t \in l, \text{Iic}(\mathcal{P}(t)) \subseteq S$

Informal description

For a filter $l$ on a type $\alpha$ and a subset $S$ of the space of filters on $\alpha$, $S$ is a neighborhood of $l$ in the topology on $\text{Filter } \alpha$ if and only if there exists a set $t \in l$ such that the left-infinite right-closed interval $\{l' \in \text{Filter } \alpha \mid l' \leq \mathcal{P}(t)\}$ is contained in $S$.

Filter.mem_nhds_iff' theorem

{l : Filter α} {S : Set (Filter α)} : S ∈ 𝓝 l ↔ ∃ t ∈ l, ∀ ⦃l' : Filter α⦄, t ∈ l' → l' ∈ S

Full source

theorem mem_nhds_iff' {l : Filter α} {S : Set (Filter α)} :
    S ∈ 𝓝 lS ∈ 𝓝 l ↔ ∃ t ∈ l, ∀ ⦃l' : Filter α⦄, t ∈ l' → l' ∈ S :=
  l.basis_sets.nhds'.mem_iff

Neighborhood Characterization in Filter Topology via Membership

Informal description

For a filter $l$ on a type $\alpha$ and a subset $S$ of the space of filters on $\alpha$, $S$ is a neighborhood of $l$ in the topology on $\text{Filter } \alpha$ if and only if there exists a set $t \in l$ such that for any filter $l'$ on $\alpha$, if $t \in l'$ then $l' \in S$.

Filter.nhds_bot theorem

: 𝓝 (⊥ : Filter α) = pure ⊥

Full source

@[simp]
theorem nhds_bot : 𝓝 (⊥ : Filter α) = pure ⊥ := by
  simp [nhds_eq, Function.comp_def, lift'_bot monotone_principal.Iic]

Neighborhood Filter of Bottom Filter is Pure Singleton

Informal description

The neighborhood filter of the bottom element $\bot$ in the space of filters on a type $\alpha$ is equal to the pure filter $\{\bot\}$.

Filter.nhds_top theorem

: 𝓝 (⊤ : Filter α) = ⊤

Full source

@[simp]
theorem nhds_top : 𝓝 (⊤ : Filter α) = ⊤ := by simp [nhds_eq]

Neighborhood Filter of Top Filter is Trivial

Informal description

The neighborhood filter of the top element $\top$ in the space of filters on a type $\alpha$ is equal to the trivial filter $\top$ itself.

Filter.nhds_principal theorem

(s : Set α) : 𝓝 (𝓟 s) = 𝓟 (Iic (𝓟 s))

Full source

@[simp]
theorem nhds_principal (s : Set α) : 𝓝 (𝓟 s) = 𝓟 (Iic (𝓟 s)) :=
  (hasBasis_principal s).nhds.eq_of_same_basis (hasBasis_principal _)

Neighborhood Filter of Principal Filter Equals Principal Filter of Lower Set

Informal description

For any subset $s$ of a type $\alpha$, the neighborhood filter of the principal filter $\mathfrak{P}(s)$ in the topology on $\text{Filter } \alpha$ is equal to the principal filter generated by the left-infinite right-closed interval $(-\infty, \mathfrak{P}(s)]$, i.e., \[ \mathcal{N}(\mathfrak{P}(s)) = \mathfrak{P}\left((-\infty, \mathfrak{P}(s)]\right). \]

Filter.nhds_pure theorem

(x : α) : 𝓝 (pure x : Filter α) = 𝓟 {⊥, pure x}

Full source

@[simp]
theorem nhds_pure (x : α) : 𝓝 (pure x : Filter α) = 𝓟 {⊥, pure x} := by
  rw [← principal_singleton, nhds_principal, principal_singleton, Iic_pure]

Neighborhood Filter of Pure Filter Equals Principal Filter of Minimal Elements

Informal description

For any element $x$ of type $\alpha$, the neighborhood filter of the pure filter $\text{pure } x$ in the topology on $\text{Filter } \alpha$ is equal to the principal filter generated by the set $\{\bot, \text{pure } x\}$, i.e., \[ \mathcal{N}(\text{pure } x) = \mathfrak{P}\left(\{\bot, \text{pure } x\}\right). \]

Filter.nhds_iInf theorem

(f : ι → Filter α) : 𝓝 (⨅ i, f i) = ⨅ i, 𝓝 (f i)

Full source

@[simp]
protected theorem nhds_iInf (f : ι → Filter α) : 𝓝 (⨅ i, f i) = ⨅ i, 𝓝 (f i) := by
  simp only [nhds_eq]
  apply lift'_iInf_of_map_univ <;> simp

Neighborhood Filter of Infimum of Filters Equals Infimum of Neighborhood Filters

Informal description

For any family of filters $(f_i)_{i \in \iota}$ on a type $\alpha$, the neighborhood filter of their infimum $\bigsqcap_i f_i$ in the topology on $\text{Filter } \alpha$ is equal to the infimum of the neighborhood filters of each $f_i$, i.e., \[ \mathcal{N}\left(\bigsqcap_i f_i\right) = \bigsqcap_i \mathcal{N}(f_i). \]

Filter.nhds_inf theorem

(l₁ l₂ : Filter α) : 𝓝 (l₁ ⊓ l₂) = 𝓝 l₁ ⊓ 𝓝 l₂

Full source

@[simp]
protected theorem nhds_inf (l₁ l₂ : Filter α) : 𝓝 (l₁ ⊓ l₂) = 𝓝𝓝 l₁ ⊓ 𝓝 l₂ := by
  simpa only [iInf_bool_eq] using Filter.nhds_iInf fun b => cond b l₁ l₂

Neighborhood Filter of Infimum Equals Infimum of Neighborhood Filters

Informal description

For any two filters $l_1$ and $l_2$ on a type $\alpha$, the neighborhood filter of their infimum $l_1 \sqcap l_2$ in the topology on $\text{Filter } \alpha$ is equal to the infimum of their neighborhood filters, i.e., \[ \mathcal{N}(l_1 \sqcap l_2) = \mathcal{N}(l_1) \sqcap \mathcal{N}(l_2). \]

Filter.monotone_nhds theorem

: Monotone (𝓝 : Filter α → Filter (Filter α))

Full source

theorem monotone_nhds : Monotone (𝓝 : Filter α → Filter (Filter α)) :=
  Monotone.of_map_inf Filter.nhds_inf

Monotonicity of the Neighborhood Filter Map

Informal description

The neighborhood map $\mathcal{N} \colon \text{Filter } \alpha \to \text{Filter } (\text{Filter } \alpha)$ is monotone with respect to the partial order on filters. That is, for any two filters $l_1$ and $l_2$ on $\alpha$, if $l_1 \leq l_2$, then $\mathcal{N}(l_1) \leq \mathcal{N}(l_2)$.

Filter.sInter_nhds theorem

(l : Filter α) : ⋂₀ {s | s ∈ 𝓝 l} = Iic l

Full source

theorem sInter_nhds (l : Filter α) : ⋂₀ { s | s ∈ 𝓝 l } = Iic l := by
  simp_rw [nhds_eq, Function.comp_def, sInter_lift'_sets monotone_principal.Iic, Iic,
    le_principal_iff, ← setOf_forall, ← Filter.le_def]

Intersection of Neighborhoods of a Filter Equals Lower Set

Informal description

For any filter $l$ on a type $\alpha$, the intersection of all neighborhoods of $l$ in the topology on $\text{Filter } \alpha$ is equal to the left-infinite right-closed interval $\{l' \in \text{Filter } \alpha \mid l' \leq l\}$. That is, \[ \bigcap_{s \in \mathcal{N}(l)} s = \{l' \mid l' \leq l\}. \]

Filter.nhds_mono theorem

{l₁ l₂ : Filter α} : 𝓝 l₁ ≤ 𝓝 l₂ ↔ l₁ ≤ l₂

Full source

@[simp]
theorem nhds_mono {l₁ l₂ : Filter α} : 𝓝𝓝 l₁ ≤ 𝓝 l₂ ↔ l₁ ≤ l₂ := by
  refine ⟨fun h => ?_, fun h => monotone_nhds h⟩
  rw [← Iic_subset_Iic, ← sInter_nhds, ← sInter_nhds]
  exact sInter_subset_sInter h

Monotonicity of Neighborhood Filters: $\mathcal{N}(l_1) \leq \mathcal{N}(l_2) \leftrightarrow l_1 \leq l_2$

Informal description

For any two filters $l_1$ and $l_2$ on a type $\alpha$, the neighborhood filter $\mathcal{N}(l_1)$ is less than or equal to $\mathcal{N}(l_2)$ if and only if $l_1 \leq l_2$ in the partial order on filters.

Filter.mem_interior theorem

{s : Set (Filter α)} {l : Filter α} : l ∈ interior s ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s

Full source

protected theorem mem_interior {s : Set (Filter α)} {l : Filter α} :
    l ∈ interior sl ∈ interior s ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s := by
  rw [mem_interior_iff_mem_nhds, Filter.mem_nhds_iff]

Characterization of Filter Interior via Basic Open Sets

Informal description

For a set $s$ of filters on a type $\alpha$ and a filter $l$ on $\alpha$, $l$ is in the interior of $s$ if and only if there exists a set $t \in l$ such that every filter containing $t$ is also in $s$. In other words, \[ l \in \text{interior}(s) \leftrightarrow \exists t \in l, \{l' \mid t \in l'\} \subseteq s. \]

Filter.mem_closure theorem

{s : Set (Filter α)} {l : Filter α} : l ∈ closure s ↔ ∀ t ∈ l, ∃ l' ∈ s, t ∈ l'

Full source

protected theorem mem_closure {s : Set (Filter α)} {l : Filter α} :
    l ∈ closure sl ∈ 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, Classical.not_not, exists_prop, not_and, and_comm, subset_def, mem_Iic,
    le_principal_iff]

Characterization of Filter Closure via Membership

Informal description

A filter $l$ on a type $\alpha$ belongs to the topological closure of a set $s$ of filters if and only if for every set $t$ in $l$, there exists a filter $l'$ in $s$ such that $t$ is also in $l'$.

Filter.closure_singleton theorem

(l : Filter α) : closure { l } = Ici l

Full source

@[simp]
protected theorem closure_singleton (l : Filter α) : closure {l} = Ici l := by
  ext l'
  simp [Filter.mem_closure, Filter.le_def]

Closure of a Singleton Filter Equals the Set of Finer Filters

Informal description

For any filter $l$ on a type $\alpha$, the topological closure of the singleton set $\{l\}$ in the space of filters is equal to the set of all filters that are finer than $l$, i.e., $\overline{\{l\}} = \{l' \mid l \leq l'\}$.

Filter.specializes_iff_le theorem

{l₁ l₂ : Filter α} : l₁ ⤳ l₂ ↔ l₁ ≤ l₂

Full source

@[simp]
theorem specializes_iff_le {l₁ l₂ : Filter α} : l₁ ⤳ l₂l₁ ⤳ l₂ ↔ l₁ ≤ l₂ := by
  simp only [specializes_iff_closure_subset, Filter.closure_singleton, Ici_subset_Ici]

Specialization Order on Filters Coincides with Fineness Order

Informal description

For any two filters $l_1$ and $l_2$ on a type $\alpha$, the specialization relation $l_1 \rightsquigarrow l_2$ holds if and only if $l_1$ is finer than $l_2$, i.e., $l_1 \leq l_2$.

Filter.instT0Space instance

: T0Space (Filter α)

Full source

instance : T0Space (Filter α) :=
  ⟨fun _ _ h => (specializes_iff_le.1 h.specializes).antisymm
    (specializes_iff_le.1 h.symm.specializes)⟩

The Space of Filters is T₀

Informal description

The space of filters $\text{Filter } \alpha$ on a type $\alpha$ is a T₀ space with respect to the topology generated by the basic open sets $\{l : \text{Filter } \alpha \mid s \in l\}$ for each subset $s \subseteq \alpha$.

Filter.nhds_atTop theorem

[Preorder α] : 𝓝 atTop = ⨅ x : α, 𝓟 (Iic (𝓟 (Ici x)))

Full source

theorem nhds_atTop [Preorder α] : 𝓝 atTop = ⨅ x : α, 𝓟 (Iic (𝓟 (Ici x))) := by
  simp only [atTop, Filter.nhds_iInf, nhds_principal]

Neighborhood Filter of `atTop` Equals Infimum of Principal Filters of Lower Sets of Upper Sets

Informal description

For a preorder $\alpha$, the neighborhood filter of the `atTop` filter in the topology on $\text{Filter } \alpha$ is equal to the infimum over all $x \in \alpha$ of the principal filters generated by the sets $\{l : \text{Filter } \alpha \mid [x, \infty) \in l\}$. In other words, \[ \mathcal{N}(\text{atTop}) = \bigsqcap_{x \in \alpha} \mathfrak{P}\left((-\infty, \mathfrak{P}([x, \infty))]\right). \]

Filter.tendsto_nhds_atTop_iff theorem

[Preorder β] {l : Filter α} {f : α → Filter β} : Tendsto f l (𝓝 atTop) ↔ ∀ y, ∀ᶠ a in l, Ici y ∈ f a

Full source

protected theorem tendsto_nhds_atTop_iff [Preorder β] {l : Filter α} {f : α → Filter β} :
    TendstoTendsto f l (𝓝 atTop) ↔ ∀ y, ∀ᶠ a in l, Ici y ∈ f a := by
  simp only [nhds_atTop, tendsto_iInf, tendsto_principal, mem_Iic, le_principal_iff]

Characterization of Convergence to the Neighborhood Filter of $\text{atTop}$ in the Space of Filters

Informal description

Let $\beta$ be a preorder, $l$ be a filter on a type $\alpha$, and $f : \alpha \to \text{Filter } \beta$ be a function. The function $f$ tends to the neighborhood filter of $\text{atTop}$ in the topology on $\text{Filter } \beta$ if and only if for every $y \in \beta$, the set $\{a \in \alpha \mid [y, \infty) \in f(a)\}$ is eventually in $l$. In other words, \[ f \text{ tends to } \mathcal{N}(\text{atTop}) \text{ if and only if } \forall y \in \beta, \exists U \in l, \forall a \in U, [y, \infty) \in f(a). \]

Filter.nhds_atBot theorem

[Preorder α] : 𝓝 atBot = ⨅ x : α, 𝓟 (Iic (𝓟 (Iic x)))

Full source

theorem nhds_atBot [Preorder α] : 𝓝 atBot = ⨅ x : α, 𝓟 (Iic (𝓟 (Iic x))) :=
  @nhds_atTop αᵒᵈ _

Neighborhood Filter of `atBot` as Infimum of Principal Filters of Lower Sets

Informal description

For a preordered set $\alpha$, the neighborhood filter of the `atBot` filter in the topology on $\text{Filter } \alpha$ is equal to the infimum over all $x \in \alpha$ of the principal filters generated by the sets $\{l : \text{Filter } \alpha \mid (-\infty, x] \in l\}$. In other words, \[ \mathcal{N}(\text{atBot}) = \bigsqcap_{x \in \alpha} \mathcal{P}\left(\{l \mid (-\infty, x] \in l\}\right). \]

Filter.tendsto_nhds_atBot_iff theorem

[Preorder β] {l : Filter α} {f : α → Filter β} : Tendsto f l (𝓝 atBot) ↔ ∀ y, ∀ᶠ a in l, Iic y ∈ f a

Full source

protected theorem tendsto_nhds_atBot_iff [Preorder β] {l : Filter α} {f : α → Filter β} :
    TendstoTendsto f l (𝓝 atBot) ↔ ∀ y, ∀ᶠ a in l, Iic y ∈ f a :=
  @Filter.tendsto_nhds_atTop_iff α βᵒᵈ _ _ _

Characterization of convergence to the neighborhood filter of $\text{atBot}$ in the space of filters

Informal description

Let $\beta$ be a preorder, $l$ be a filter on a type $\alpha$, and $f : \alpha \to \text{Filter } \beta$ be a function. The function $f$ tends to the neighborhood filter of $\text{atBot}$ in the topology on $\text{Filter } \beta$ if and only if for every $y \in \beta$, the set $\{a \in \alpha \mid (-\infty, y] \in f(a)\}$ is eventually in $l$. In other words, \[ f \text{ tends to } \mathcal{N}(\text{atBot}) \text{ if and only if } \forall y \in \beta, \exists U \in l, \forall a \in U, (-\infty, y] \in f(a). \]

Filter.nhds_nhds theorem

(x : X) : 𝓝 (𝓝 x) = ⨅ (s : Set X) (_ : IsOpen s) (_ : x ∈ s), 𝓟 (Iic (𝓟 s))

Full source

theorem nhds_nhds (x : X) :
    𝓝 (𝓝 x) = ⨅ (s : Set X) (_ : IsOpen s) (_ : x ∈ s), 𝓟 (Iic (𝓟 s)) := by
  simp only [(nhds_basis_opens x).nhds.eq_biInf, iInf_and, @iInf_comm _ (_ ∈ _)]

Neighborhood filter of the neighborhood filter at a point in the filter topology

Informal description

For any point $x$ in a topological space $X$, the neighborhood filter $\mathcal{N}(\mathcal{N}(x))$ in the topology on $\text{Filter } X$ is equal to the infimum over all open sets $s \subseteq X$ containing $x$ of the principal filter generated by the set $\{l \in \text{Filter } X \mid s \in l\}$. In other words, $\mathcal{N}(\mathcal{N}(x)) = \bigsqcap_{s \text{ open}, x \in s} \mathcal{P}(\{l \mid s \in l\})$.

Filter.isInducing_nhds theorem

: IsInducing (𝓝 : X → Filter X)

Full source

theorem isInducing_nhds : IsInducing (𝓝 : X → Filter X) :=
  isInducing_iff_nhds.2 fun x =>
    (nhds_def' _).trans <| by
      simp +contextual only [nhds_nhds, comap_iInf, comap_principal,
        Iic_principal, preimage_setOf_eq, ← mem_interior_iff_mem_nhds, setOf_mem_eq,
        IsOpen.interior_eq]

Neighborhood Map is Inducing

Informal description

The neighborhood map $\mathcal{N} \colon X \to \text{Filter } X$ from a topological space $X$ to its space of filters is inducing, meaning that for every point $x \in X$, the neighborhood filter $\mathcal{N}_x$ of $x$ in $X$ is equal to the preimage under $\mathcal{N}$ of the neighborhood filter of $\mathcal{N}(x)$ in the topology on $\text{Filter } X$.

Filter.continuous_nhds theorem

: Continuous (𝓝 : X → Filter X)

Full source

@[continuity]
theorem continuous_nhds : Continuous (𝓝 : X → Filter X) :=
  isInducing_nhds.continuous

Continuity of the Neighborhood Map in the Filter Topology

Informal description

The neighborhood map $\mathcal{N} \colon X \to \text{Filter } X$ from a topological space $X$ to its space of filters is continuous with respect to the topology on $\text{Filter } X$.

Filter.Tendsto.nhds theorem

{f : α → X} {l : Filter α} {x : X} (h : Tendsto f l (𝓝 x)) : Tendsto (𝓝 ∘ f) l (𝓝 (𝓝 x))

Full source

protected theorem Tendsto.nhds {f : α → X} {l : Filter α} {x : X} (h : Tendsto f l (𝓝 x)) :
    Tendsto (𝓝𝓝 ∘ f) l (𝓝 (𝓝 x)) :=
  (continuous_nhds.tendsto _).comp h

Neighborhood Filter Convergence under Function Composition

Informal description

Let $X$ be a topological space and $f \colon \alpha \to X$ be a function. If $f$ tends to a neighborhood $\mathcal{N}_x$ of $x \in X$ along a filter $l$ on $\alpha$, then the composition $\mathcal{N} \circ f$ tends to the neighborhood filter of $\mathcal{N}_x$ in the space of filters on $X$ along the same filter $l$. In other words, if $\lim_{y \to l} f(y) = x$, then $\lim_{y \to l} \mathcal{N}_{f(y)} = \mathcal{N}_x$ in the topology on $\text{Filter } X$.

ContinuousWithinAt.nhds theorem

(h : ContinuousWithinAt f s x) : ContinuousWithinAt (𝓝 ∘ f) s x

Full source

protected nonrec theorem ContinuousWithinAt.nhds (h : ContinuousWithinAt f s x) :
    ContinuousWithinAt (𝓝𝓝 ∘ f) s x :=
  h.nhds

Continuity of Neighborhood Filter Composition within a Subset

Informal description

Let $X$ and $Y$ be topological spaces, $f \colon X \to Y$ a function, $s \subseteq X$ a subset, and $x \in X$. If $f$ is continuous within $s$ at $x$, then the composition $\mathcal{N} \circ f$ (where $\mathcal{N}$ is the neighborhood filter map) is also continuous within $s$ at $x$.

ContinuousAt.nhds theorem

(h : ContinuousAt f x) : ContinuousAt (𝓝 ∘ f) x

Full source

protected nonrec theorem ContinuousAt.nhds (h : ContinuousAt f x) : ContinuousAt (𝓝𝓝 ∘ f) x :=
  h.nhds

Continuity of Neighborhood Composition at a Point

Informal description

Let $X$ and $Y$ be topological spaces and $f \colon X \to Y$ be a function. If $f$ is continuous at a point $x \in X$, then the composition $\mathcal{N} \circ f \colon X \to \text{Filter } Y$ is also continuous at $x$, where $\mathcal{N} \colon Y \to \text{Filter } Y$ is the neighborhood map.

ContinuousOn.nhds theorem

(h : ContinuousOn f s) : ContinuousOn (𝓝 ∘ f) s

Full source

protected nonrec theorem ContinuousOn.nhds (h : ContinuousOn f s) : ContinuousOn (𝓝𝓝 ∘ f) s :=
  fun x hx => (h x hx).nhds

Continuity of Neighborhood Composition on a Subset

Informal description

Let $X$ and $Y$ be topological spaces, $f \colon X \to Y$ a function, and $s \subseteq X$ a subset. If $f$ is continuous on $s$, then the composition $\mathcal{N} \circ f$ (where $\mathcal{N} \colon Y \to \text{Filter } Y$ is the neighborhood map) is continuous on $s$.

Continuous.nhds theorem

(h : Continuous f) : Continuous (𝓝 ∘ f)

Full source

protected nonrec theorem Continuous.nhds (h : Continuous f) : Continuous (𝓝𝓝 ∘ f) :=
  Filter.continuous_nhds.comp h

Continuity of the Composition of a Continuous Function with the Neighborhood Map

Informal description

Let $X$ and $Y$ be topological spaces and $f \colon X \to Y$ be a continuous function. Then the composition $\mathcal{N} \circ f \colon X \to \text{Filter } Y$ is continuous, where $\mathcal{N} \colon Y \to \text{Filter } Y$ is the neighborhood map.

Tags