Mathlib.Topology.Neighborhoods

nhds_def' theorem

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

Full source

theorem nhds_def' (x : X) : 𝓝 x = ⨅ (s : Set X) (_ : IsOpen s) (_ : x ∈ s), 𝓟 s := by
  simp only [nhds_def, mem_setOf_eq, @and_comm (x ∈ _), iInf_and]

Neighborhood Filter as Infimum of Principal Filters of Open Neighborhoods

Informal description

For any point $x$ in a topological space $X$, the neighborhood filter $\mathcal{N}(x)$ is equal to the infimum of the principal filters $\mathcal{P}(s)$ over all open sets $s$ containing $x$, i.e., \[ \mathcal{N}(x) = \bigsqcap_{\substack{s \subseteq X \\ \text{open}, x \in s}} \mathcal{P}(s). \]

nhds_basis_opens theorem

(x : X) : (𝓝 x).HasBasis (fun s : Set X => x ∈ s ∧ IsOpen s) fun s => s

Full source

/-- The open sets containing `x` are a basis for the neighborhood filter. See `nhds_basis_opens'`
for a variant using open neighborhoods instead. -/
theorem nhds_basis_opens (x : X) :
    (𝓝 x).HasBasis (fun s : Set X => x ∈ sx ∈ s ∧ IsOpen s) fun s => s := by
  rw [nhds_def]
  exact hasBasis_biInf_principal
    (fun s ⟨has, hs⟩ t ⟨hat, ht⟩ =>
      ⟨s ∩ t, ⟨⟨has, hat⟩, IsOpen.inter hs ht⟩, ⟨inter_subset_left, inter_subset_right⟩⟩)
    ⟨univ, ⟨mem_univ x, isOpen_univ⟩⟩

Open Sets Form Basis for Neighborhood Filter at a Point

Informal description

For any point $x$ in a topological space $X$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of all open sets containing $x$. That is, the collection $\{s \subseteq X \mid x \in s \text{ and } s \text{ is open}\}$ forms a basis for $\mathcal{N}(x)$, where each basis element $s$ maps to itself under the identity function.

nhds_basis_closeds theorem

(x : X) : (𝓝 x).HasBasis (fun s : Set X => x ∉ s ∧ IsClosed s) compl

Full source

theorem nhds_basis_closeds (x : X) : (𝓝 x).HasBasis (fun s : Set X => x ∉ sx ∉ s ∧ IsClosed s) compl :=
  ⟨fun t => (nhds_basis_opens x).mem_iff.trans <|
    compl_surjective.exists.trans <| by simp only [isOpen_compl_iff, mem_compl_iff]⟩

Closed Set Complements Form Basis for Neighborhood Filter

Informal description

For any point $x$ in a topological space $X$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of the complements of all closed sets not containing $x$. That is, the collection $\{s^c \subseteq X \mid x \notin s \text{ and } s \text{ is closed}\}$ forms a basis for $\mathcal{N}(x)$, where each basis element is the complement of such a set $s$.

lift'_nhds_interior theorem

(x : X) : (𝓝 x).lift' interior = 𝓝 x

Full source

@[simp]
theorem lift'_nhds_interior (x : X) : (𝓝 x).lift' interior = 𝓝 x :=
  (nhds_basis_opens x).lift'_interior_eq_self fun _ ↦ And.right

Neighborhood Filter Invariance Under Interior Operation

Informal description

For any point $x$ in a topological space $X$, the filter obtained by applying the interior operation to all sets in the neighborhood filter $\mathcal{N}(x)$ is equal to $\mathcal{N}(x)$ itself. That is, $\text{lift}'(\text{interior}, \mathcal{N}(x)) = \mathcal{N}(x)$.

Filter.HasBasis.nhds_interior theorem

{x : X} {p : ι → Prop} {s : ι → Set X} (h : (𝓝 x).HasBasis p s) : (𝓝 x).HasBasis p (interior <| s ·)

Full source

theorem Filter.HasBasis.nhds_interior {x : X} {p : ι → Prop} {s : ι → Set X}
    (h : (𝓝 x).HasBasis p s) : (𝓝 x).HasBasis p (interior <| s ·) :=
  lift'_nhds_interior x ▸ h.lift'_interior

Neighborhood Filter Basis Preservation Under Interior Operation

Informal description

Let $X$ be a topological space and $x \in X$. Suppose the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of sets $\{s_i\}_{i \in \iota}$ indexed by some type $\iota$ with a predicate $p$. Then $\mathcal{N}(x)$ also has a basis consisting of the interiors of these sets, i.e., $\{\text{interior}(s_i)\}_{i \in \iota}$ with the same predicate $p$.

le_nhds_iff theorem

{f} : f ≤ 𝓝 x ↔ ∀ s : Set X, x ∈ s → IsOpen s → s ∈ f

Full source

/-- A filter lies below the neighborhood filter at `x` iff it contains every open set around `x`. -/
theorem le_nhds_iff {f} : f ≤ 𝓝 x ↔ ∀ s : Set X, x ∈ s → IsOpen s → s ∈ f := by simp [nhds_def]

Characterization of Filter Containment in Neighborhood Filter via Open Sets

Informal description

For any filter $f$ on a topological space $X$ and any point $x \in X$, the filter $f$ is contained in the neighborhood filter $\mathcal{N}(x)$ if and only if every open set $s$ containing $x$ belongs to $f$.

nhds_le_of_le theorem

{f} (h : x ∈ s) (o : IsOpen s) (sf : 𝓟 s ≤ f) : 𝓝 x ≤ f

Full source

/-- To show a filter is above the neighborhood filter at `x`, it suffices to show that it is above
the principal filter of some open set `s` containing `x`. -/
theorem nhds_le_of_le {f} (h : x ∈ s) (o : IsOpen s) (sf : 𝓟 s ≤ f) : 𝓝 x ≤ f := by
  rw [nhds_def]; exact iInf₂_le_of_le s ⟨h, o⟩ sf

Neighborhood Filter Containment via Open Sets

Informal description

For any filter $f$ on a topological space $X$, if there exists an open set $s \subseteq X$ containing $x$ such that the principal filter $\mathfrak{P}(s)$ is contained in $f$, then the neighborhood filter $\mathcal{N}(x)$ is also contained in $f$.

mem_nhds_iff theorem

: s ∈ 𝓝 x ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t

Full source

theorem mem_nhds_iff : s ∈ 𝓝 xs ∈ 𝓝 x ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t :=
  (nhds_basis_opens x).mem_iff.trans <| exists_congr fun _ =>
    ⟨fun h => ⟨h.2, h.1.2, h.1.1⟩, fun h => ⟨⟨h.2.2, h.2.1⟩, h.1⟩⟩

Characterization of Neighborhood Membership via Open Subsets

Informal description

A set $s$ is in the neighborhood filter $\mathcal{N}(x)$ of a point $x$ in a topological space $X$ if and only if there exists an open set $t$ such that $t \subseteq s$ and $x \in t$.

eventually_nhds_iff theorem

{p : X → Prop} : (∀ᶠ y in 𝓝 x, p y) ↔ ∃ t : Set X, (∀ y ∈ t, p y) ∧ IsOpen t ∧ x ∈ t

Full source

/-- A predicate is true in a neighborhood of `x` iff it is true for all the points in an open set
containing `x`. -/
theorem eventually_nhds_iff {p : X → Prop} :
    (∀ᶠ y in 𝓝 x, p y) ↔ ∃ t : Set X, (∀ y ∈ t, p y) ∧ IsOpen t ∧ x ∈ t :=
  mem_nhds_iff.trans <| by simp only [subset_def, exists_prop, mem_setOf_eq]

Neighborhood Criterion for Eventual Truth of Predicates

Informal description

A predicate $p$ on a topological space $X$ holds for all points in some neighborhood of $x$ if and only if there exists an open set $t$ containing $x$ such that $p(y)$ holds for all $y \in t$.

frequently_nhds_iff theorem

{p : X → Prop} : (∃ᶠ y in 𝓝 x, p y) ↔ ∀ U : Set X, x ∈ U → IsOpen U → ∃ y ∈ U, p y

Full source

theorem frequently_nhds_iff {p : X → Prop} :
    (∃ᶠ y in 𝓝 x, p y) ↔ ∀ U : Set X, x ∈ U → IsOpen U → ∃ y ∈ U, p y :=
  (nhds_basis_opens x).frequently_iff.trans <| by simp

Frequent Occurrence in Neighborhoods Criterion

Informal description

For any predicate $p$ on a topological space $X$ and any point $x \in X$, the following are equivalent: 1. The predicate $p$ holds frequently in the neighborhood filter $\mathcal{N}(x)$ of $x$, meaning there exists a set $s \in \mathcal{N}(x)$ such that $p(y)$ holds for all $y \in s$. 2. For every open set $U$ containing $x$, there exists a point $y \in U$ such that $p(y)$ holds. In other words, $p$ holds frequently near $x$ if and only if $p$ holds at some point in every open neighborhood of $x$.

mem_interior_iff_mem_nhds theorem

: x ∈ interior s ↔ s ∈ 𝓝 x

Full source

theorem mem_interior_iff_mem_nhds : x ∈ interior sx ∈ interior s ↔ s ∈ 𝓝 x :=
  mem_interior.trans mem_nhds_iff.symm

Interior-Neighborhood Equivalence: $x \in \text{interior}(s) \leftrightarrow s \in \mathcal{N}(x)$

Informal description

A point $x$ belongs to the interior of a set $s$ in a topological space if and only if $s$ is a neighborhood of $x$ (i.e., $s \in \mathcal{N}(x)$).

map_nhds theorem

{f : X → α} : map f (𝓝 x) = ⨅ s ∈ {s : Set X | x ∈ s ∧ IsOpen s}, 𝓟 (f '' s)

Full source

theorem map_nhds {f : X → α} :
    map f (𝓝 x) = ⨅ s ∈ { s : Set X | x ∈ s ∧ IsOpen s }, 𝓟 (f '' s) :=
  ((nhds_basis_opens x).map f).eq_biInf

Image of Neighborhood Filter under a Function

Informal description

For any function $f : X \to \alpha$ and any point $x \in X$, the image of the neighborhood filter $\mathcal{N}(x)$ under $f$ is equal to the infimum of the principal filters generated by the images of all open sets $s \subseteq X$ containing $x$. That is, \[ \text{map}\, f\, \mathcal{N}(x) = \bigsqcap_{\substack{s \subseteq X \\ x \in s \\ \text{$s$ is open}}} \mathcal{P}(f(s)), \] where $\mathcal{P}(f(s))$ denotes the principal filter generated by the image $f(s)$.

mem_of_mem_nhds theorem

: s ∈ 𝓝 x → x ∈ s

Full source

theorem mem_of_mem_nhds : s ∈ 𝓝 x → x ∈ s := fun H =>
  let ⟨_t, ht, _, hs⟩ := mem_nhds_iff.1 H; ht hs

Neighborhood Membership Implies Point Membership

Informal description

If a set $s$ is in the neighborhood filter $\mathcal{N}(x)$ of a point $x$ in a topological space, then $x$ is an element of $s$.

Filter.Eventually.self_of_nhds theorem

{p : X → Prop} (h : ∀ᶠ y in 𝓝 x, p y) : p x

Full source

/-- If a predicate is true in a neighborhood of `x`, then it is true for `x`. -/
theorem Filter.Eventually.self_of_nhds {p : X → Prop} (h : ∀ᶠ y in 𝓝 x, p y) : p x :=
  mem_of_mem_nhds h

Neighborhood Eventual Truth Implies Point Truth

Informal description

If a predicate $p$ holds for all points $y$ in some neighborhood of $x$ in a topological space, then $p$ holds at $x$ itself.

IsOpen.mem_nhds theorem

(hs : IsOpen s) (hx : x ∈ s) : s ∈ 𝓝 x

Full source

theorem IsOpen.mem_nhds (hs : IsOpen s) (hx : x ∈ s) : s ∈ 𝓝 x :=
  mem_nhds_iff.2 ⟨s, Subset.refl _, hs, hx⟩

Open Sets are Neighborhoods of Their Points

Informal description

For any open set $s$ in a topological space and any point $x \in s$, the set $s$ belongs to the neighborhood filter $\mathcal{N}(x)$ of $x$.

IsOpen.mem_nhds_iff theorem

(hs : IsOpen s) : s ∈ 𝓝 x ↔ x ∈ s

Full source

protected theorem IsOpen.mem_nhds_iff (hs : IsOpen s) : s ∈ 𝓝 xs ∈ 𝓝 x ↔ x ∈ s :=
  ⟨mem_of_mem_nhds, fun hx => mem_nhds_iff.2 ⟨s, Subset.rfl, hs, hx⟩⟩

Open Set Membership in Neighborhood Filter Characterized by Point Membership

Informal description

For an open set $s$ in a topological space and a point $x$, the set $s$ belongs to the neighborhood filter $\mathcal{N}(x)$ of $x$ if and only if $x$ is an element of $s$.

IsClosed.compl_mem_nhds theorem

(hs : IsClosed s) (hx : x ∉ s) : sᶜ ∈ 𝓝 x

Full source

theorem IsClosed.compl_mem_nhds (hs : IsClosed s) (hx : x ∉ s) : sᶜsᶜ ∈ 𝓝 x :=
  hs.isOpen_compl.mem_nhds (mem_compl hx)

Complement of Closed Set is Neighborhood of Exterior Points

Informal description

For any closed set $s$ in a topological space and any point $x$ not in $s$, the complement $s^c$ belongs to the neighborhood filter $\mathcal{N}(x)$ of $x$.

IsOpen.eventually_mem theorem

(hs : IsOpen s) (hx : x ∈ s) : ∀ᶠ x in 𝓝 x, x ∈ s

Full source

theorem IsOpen.eventually_mem (hs : IsOpen s) (hx : x ∈ s) :
    ∀ᶠ x in 𝓝 x, x ∈ s :=
  IsOpen.mem_nhds hs hx

Open Sets Contain Neighborhoods of Their Points

Informal description

For any open set $s$ in a topological space and any point $x \in s$, the set $s$ contains all points in some neighborhood of $x$, i.e., $\exists U \in \mathcal{N}(x), U \subseteq s$.

nhds_basis_opens' theorem

(x : X) : (𝓝 x).HasBasis (fun s : Set X => s ∈ 𝓝 x ∧ IsOpen s) fun x => x

Full source

/-- The open neighborhoods of `x` are a basis for the neighborhood filter. See `nhds_basis_opens`
for a variant using open sets around `x` instead. -/
theorem nhds_basis_opens' (x : X) :
    (𝓝 x).HasBasis (fun s : Set X => s ∈ 𝓝 xs ∈ 𝓝 x ∧ IsOpen s) fun x => x := by
  convert nhds_basis_opens x using 2
  exact and_congr_left_iff.2 IsOpen.mem_nhds_iff

Open Neighborhoods Form Basis for Neighborhood Filter at a Point

Informal description

For any point $x$ in a topological space $X$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of all open sets that are neighborhoods of $x$. That is, the collection $\{s \subseteq X \mid s \in \mathcal{N}(x) \text{ and } s \text{ is open}\}$ forms a basis for $\mathcal{N}(x)$, where each basis element $s$ maps to itself under the identity function.

exists_open_set_nhds theorem

{U : Set X} (h : ∀ x ∈ s, U ∈ 𝓝 x) : ∃ V : Set X, s ⊆ V ∧ IsOpen V ∧ V ⊆ U

Full source

/-- If `U` is a neighborhood of each point of a set `s` then it is a neighborhood of `s`:
it contains an open set containing `s`. -/
theorem exists_open_set_nhds {U : Set X} (h : ∀ x ∈ s, U ∈ 𝓝 x) :
    ∃ V : Set X, s ⊆ V ∧ IsOpen V ∧ V ⊆ U :=
  ⟨interior U, fun x hx => mem_interior_iff_mem_nhds.2 <| h x hx, isOpen_interior, interior_subset⟩

Existence of Open Neighborhood Covering a Set

Informal description

For any set $U$ in a topological space $X$, if $U$ is a neighborhood of every point $x$ in a subset $s \subseteq X$, then there exists an open set $V$ such that $s \subseteq V$, $V$ is open, and $V \subseteq U$.

exists_open_set_nhds' theorem

{U : Set X} (h : U ∈ ⨆ x ∈ s, 𝓝 x) : ∃ V : Set X, s ⊆ V ∧ IsOpen V ∧ V ⊆ U

Full source

/-- If `U` is a neighborhood of each point of a set `s` then it is a neighborhood of s:
it contains an open set containing `s`. -/
theorem exists_open_set_nhds' {U : Set X} (h : U ∈ ⨆ x ∈ s, 𝓝 x) :
    ∃ V : Set X, s ⊆ V ∧ IsOpen V ∧ V ⊆ U :=
  exists_open_set_nhds (by simpa using h)

Existence of Open Set from Supremum of Neighborhood Filters

Informal description

For any set $U$ in a topological space $X$, if $U$ belongs to the supremum of neighborhood filters $\bigsqcup_{x \in s} \mathcal{N}(x)$, then there exists an open set $V$ such that $s \subseteq V$, $V$ is open, and $V \subseteq U$.

Filter.Eventually.eventually_nhds theorem

{p : X → Prop} (h : ∀ᶠ y in 𝓝 x, p y) : ∀ᶠ y in 𝓝 x, ∀ᶠ x in 𝓝 y, p x

Full source

/-- If a predicate is true in a neighbourhood of `x`, then for `y` sufficiently close
to `x` this predicate is true in a neighbourhood of `y`. -/
theorem Filter.Eventually.eventually_nhds {p : X → Prop} (h : ∀ᶠ y in 𝓝 x, p y) :
    ∀ᶠ y in 𝓝 x, ∀ᶠ x in 𝓝 y, p x :=
  let ⟨t, htp, hto, ha⟩ := eventually_nhds_iff.1 h
  eventually_nhds_iff.2 ⟨t, fun _x hx => eventually_nhds_iff.2 ⟨t, htp, hto, hx⟩, hto, ha⟩

Neighborhood Propagation of Predicates

Informal description

For any predicate $p$ on a topological space $X$ and any point $x \in X$, if $p(y)$ holds for all $y$ in some neighborhood of $x$, then there exists a neighborhood of $x$ such that for every $y$ in this neighborhood, $p(x)$ holds for all $x$ in some neighborhood of $y$.

eventually_eventually_nhds theorem

{p : X → Prop} : (∀ᶠ y in 𝓝 x, ∀ᶠ x in 𝓝 y, p x) ↔ ∀ᶠ x in 𝓝 x, p x

Full source

@[simp]
theorem eventually_eventually_nhds {p : X → Prop} :
    (∀ᶠ y in 𝓝 x, ∀ᶠ x in 𝓝 y, p x) ↔ ∀ᶠ x in 𝓝 x, p x :=
  ⟨fun h => h.self_of_nhds, fun h => h.eventually_nhds⟩

Equivalence of Local and Pointwise Eventual Truth in Neighborhoods

Informal description

For any predicate $p$ on a topological space $X$ and any point $x \in X$, the following are equivalent: 1. There exists a neighborhood of $x$ such that for every $y$ in this neighborhood, $p$ holds for all $x'$ in some neighborhood of $y$. 2. The predicate $p$ holds for all $x'$ in some neighborhood of $x$. In other words, $p$ holds eventually near $x$ if and only if there exists a neighborhood of $x$ where $p$ holds eventually near each of its points.

frequently_frequently_nhds theorem

{p : X → Prop} : (∃ᶠ x' in 𝓝 x, ∃ᶠ x'' in 𝓝 x', p x'') ↔ ∃ᶠ x in 𝓝 x, p x

Full source

@[simp]
theorem frequently_frequently_nhds {p : X → Prop} :
    (∃ᶠ x' in 𝓝 x, ∃ᶠ x'' in 𝓝 x', p x'') ↔ ∃ᶠ x in 𝓝 x, p x := by
  rw [← not_iff_not]
  simp only [not_frequently, eventually_eventually_nhds]

Frequently in Neighborhoods Equivalence: $(\exists^f x' \text{ near } x, \exists^f x'' \text{ near } x', p(x'')) \leftrightarrow \exists^f x \text{ near } x, p(x)$

Informal description

For any predicate $p$ on a topological space $X$ and any point $x \in X$, the following are equivalent: 1. There exists a neighborhood of $x$ where $p$ holds frequently in some neighborhood of each point in that neighborhood. 2. The predicate $p$ holds frequently in the neighborhood of $x$. In other words, $p$ holds frequently near $x$ if and only if there exists a neighborhood of $x$ such that for every point $x'$ in that neighborhood, $p$ holds frequently in some neighborhood of $x'$.

eventually_mem_nhds_iff theorem

: (∀ᶠ x' in 𝓝 x, s ∈ 𝓝 x') ↔ s ∈ 𝓝 x

Full source

@[simp]
theorem eventually_mem_nhds_iff : (∀ᶠ x' in 𝓝 x, s ∈ 𝓝 x') ↔ s ∈ 𝓝 x :=
  eventually_eventually_nhds

Neighborhood Membership Criterion: $(\forall^e x' \text{ near } x, s \text{ is a neighborhood of } x') \leftrightarrow s \text{ is a neighborhood of } x$

Informal description

For any subset $s$ of a topological space $X$ and any point $x \in X$, the following are equivalent: 1. There exists a neighborhood of $x$ such that $s$ is a neighborhood of every point in that neighborhood. 2. The subset $s$ is a neighborhood of $x$. In other words, $s$ is a neighborhood of $x$ if and only if there exists a neighborhood of $x$ where $s$ is a neighborhood of each of its points.

nhds_bind_nhds theorem

: (𝓝 x).bind 𝓝 = 𝓝 x

Full source

@[simp]
theorem nhds_bind_nhds : (𝓝 x).bind 𝓝 = 𝓝 x :=
  Filter.ext fun _ => eventually_eventually_nhds

Neighborhood Filter Idempotence: $\mathcal{N}_x \bind \mathcal{N} = \mathcal{N}_x$

Informal description

For any point $x$ in a topological space $X$, the neighborhood filter $\mathcal{N}_x$ satisfies $\mathcal{N}_x \bind \mathcal{N} = \mathcal{N}_x$, where $\bind$ denotes the monadic bind operation on filters.

eventually_eventuallyEq_nhds theorem

{f g : X → α} : (∀ᶠ y in 𝓝 x, f =ᶠ[𝓝 y] g) ↔ f =ᶠ[𝓝 x] g

Full source

@[simp]
theorem eventually_eventuallyEq_nhds {f g : X → α} :
    (∀ᶠ y in 𝓝 x, f =ᶠ[𝓝 y] g) ↔ f =ᶠ[𝓝 x] g :=
  eventually_eventually_nhds

Equivalence of Local and Pointwise Eventual Equality in Neighborhoods

Informal description

For any functions $f, g : X \to \alpha$ and any point $x$ in a topological space $X$, the following are equivalent: 1. There exists a neighborhood of $x$ such that for every $y$ in this neighborhood, $f$ and $g$ are eventually equal in a neighborhood of $y$. 2. The functions $f$ and $g$ are eventually equal in a neighborhood of $x$. In other words, $f$ and $g$ are eventually equal near $x$ if and only if there exists a neighborhood of $x$ where $f$ and $g$ are eventually equal near each of its points.

eventually_eventuallyLE_nhds theorem

[LE α] {f g : X → α} : (∀ᶠ y in 𝓝 x, f ≤ᶠ[𝓝 y] g) ↔ f ≤ᶠ[𝓝 x] g

Full source

@[simp]
theorem eventually_eventuallyLE_nhds [LE α] {f g : X → α} :
    (∀ᶠ y in 𝓝 x, f ≤ᶠ[𝓝 y] g) ↔ f ≤ᶠ[𝓝 x] g :=
  eventually_eventually_nhds

Equivalence of Local and Pointwise Eventual Inequality in Neighborhoods

Informal description

Let $X$ be a topological space and $\alpha$ a type with a preorder $\leq$. For any two functions $f, g : X \to \alpha$ and any point $x \in X$, the following are equivalent: 1. There exists a neighborhood of $x$ such that for every $y$ in this neighborhood, $f \leq g$ holds eventually in the neighborhood filter of $y$. 2. The inequality $f \leq g$ holds eventually in the neighborhood filter of $x$. In other words, $f \leq g$ holds eventually near $x$ if and only if there exists a neighborhood of $x$ where $f \leq g$ holds eventually near each of its points.

Filter.EventuallyEq.eventuallyEq_nhds theorem

{f g : X → α} (h : f =ᶠ[𝓝 x] g) : ∀ᶠ y in 𝓝 x, f =ᶠ[𝓝 y] g

Full source

/-- If two functions are equal in a neighbourhood of `x`, then for `y` sufficiently close
to `x` these functions are equal in a neighbourhood of `y`. -/
theorem Filter.EventuallyEq.eventuallyEq_nhds {f g : X → α} (h : f =ᶠ[𝓝 x] g) :
    ∀ᶠ y in 𝓝 x, f =ᶠ[𝓝 y] g :=
  h.eventually_nhds

Local Equality of Functions Propagates to Nearby Points

Informal description

For any two functions $f, g : X \to \alpha$ and any point $x \in X$, if $f$ and $g$ are equal in a neighborhood of $x$, then there exists a neighborhood of $x$ such that for every $y$ in this neighborhood, $f$ and $g$ are equal in a neighborhood of $y$.

Filter.EventuallyLE.eventuallyLE_nhds theorem

[LE α] {f g : X → α} (h : f ≤ᶠ[𝓝 x] g) : ∀ᶠ y in 𝓝 x, f ≤ᶠ[𝓝 y] g

Full source

/-- If `f x ≤ g x` in a neighbourhood of `x`, then for `y` sufficiently close to `x` we have
`f x ≤ g x` in a neighbourhood of `y`. -/
theorem Filter.EventuallyLE.eventuallyLE_nhds [LE α] {f g : X → α} (h : f ≤ᶠ[𝓝 x] g) :
    ∀ᶠ y in 𝓝 x, f ≤ᶠ[𝓝 y] g :=
  h.eventually_nhds

Local Propagation of Eventual Inequality in Neighborhood Filters

Informal description

Let $X$ be a topological space and $\alpha$ a type with a preorder $\leq$. For any two functions $f, g : X \to \alpha$ and any point $x \in X$, if $f \leq g$ holds eventually in the neighborhood filter $\mathcal{N}(x)$, then there exists a neighborhood of $x$ such that for every $y$ in this neighborhood, $f \leq g$ holds eventually in the neighborhood filter $\mathcal{N}(y)$.

all_mem_nhds theorem

 (x : X) (P : Set X → Prop) (hP : ∀ s t, s ⊆ t → P s → P t) : (∀ s ∈ 𝓝 x, P s) ↔ ∀ s, IsOpen s → x ∈ s → P s

Full source

theorem all_mem_nhds (x : X) (P : Set X → Prop) (hP : ∀ s t, s ⊆ t → P s → P t) :
    (∀ s ∈ 𝓝 x, P s) ↔ ∀ s, IsOpen s → x ∈ s → P s :=
  ((nhds_basis_opens x).forall_iff hP).trans <| by simp only [@and_comm (x ∈ _), and_imp]

Characterization of Properties in Neighborhood Filter via Open Sets

Informal description

For any point $x$ in a topological space $X$ and any property $P$ of subsets of $X$ that is monotone with respect to inclusion (i.e., if $s \subseteq t$ and $P(s)$ holds, then $P(t)$ holds), the following are equivalent: 1. $P(s)$ holds for every set $s$ in the neighborhood filter $\mathcal{N}(x)$. 2. $P(s)$ holds for every open set $s$ containing $x$.

all_mem_nhds_filter theorem

 (x : X) (f : Set X → Set α) (hf : ∀ s t, s ⊆ t → f s ⊆ f t) (l : Filter α) :
  (∀ s ∈ 𝓝 x, f s ∈ l) ↔ ∀ s, IsOpen s → x ∈ s → f s ∈ l

Full source

theorem all_mem_nhds_filter (x : X) (f : Set X → Set α) (hf : ∀ s t, s ⊆ t → f s ⊆ f t)
    (l : Filter α) : (∀ s ∈ 𝓝 x, f s ∈ l) ↔ ∀ s, IsOpen s → x ∈ s → f s ∈ l :=
  all_mem_nhds _ _ fun s t ssubt h => mem_of_superset h (hf s t ssubt)

Characterization of Filter Membership via Neighborhoods and Open Sets

Informal description

For any point $x$ in a topological space $X$, any function $f \colon \mathcal{P}(X) \to \mathcal{P}(\alpha)$ that is monotone with respect to set inclusion (i.e., $s \subseteq t$ implies $f(s) \subseteq f(t)$), and any filter $l$ on $\alpha$, the following are equivalent: 1. For every neighborhood $s$ of $x$, the set $f(s)$ belongs to $l$. 2. For every open set $s$ containing $x$, the set $f(s)$ belongs to $l$.

tendsto_nhds theorem

{f : α → X} {l : Filter α} : Tendsto f l (𝓝 x) ↔ ∀ s, IsOpen s → x ∈ s → f ⁻¹' s ∈ l

Full source

theorem tendsto_nhds {f : α → X} {l : Filter α} :
    TendstoTendsto f l (𝓝 x) ↔ ∀ s, IsOpen s → x ∈ s → f ⁻¹' s ∈ l :=
  all_mem_nhds_filter _ _ (fun _ _ h => preimage_mono h) _

Characterization of Convergence to a Point via Open Neighborhoods

Informal description

For a function $f \colon \alpha \to X$ and a filter $l$ on $\alpha$, the function $f$ tends to the neighborhood filter $\mathcal{N}(x)$ as its argument tends to $l$ if and only if for every open set $s$ containing $x$, the preimage $f^{-1}(s)$ belongs to $l$.

tendsto_atTop_nhds theorem

 [Nonempty α] [SemilatticeSup α] {f : α → X} :
  Tendsto f atTop (𝓝 x) ↔ ∀ U : Set X, x ∈ U → IsOpen U → ∃ N, ∀ n, N ≤ n → f n ∈ U

Full source

theorem tendsto_atTop_nhds [Nonempty α] [SemilatticeSup α] {f : α → X} :
    TendstoTendsto f atTop (𝓝 x) ↔ ∀ U : Set X, x ∈ U → IsOpen U → ∃ N, ∀ n, N ≤ n → f n ∈ U :=
  (atTop_basis.tendsto_iff (nhds_basis_opens x)).trans <| by
    simp only [and_imp, exists_prop, true_and, mem_Ici]

Characterization of Convergence to a Point in Terms of Open Neighborhoods

Informal description

Let $X$ be a topological space and $\alpha$ be a nonempty join-semilattice. A function $f \colon \alpha \to X$ tends to the neighborhood filter $\mathcal{N}(x)$ as the argument tends to infinity if and only if for every open neighborhood $U$ of $x$, there exists an index $N \in \alpha$ such that for all $n \geq N$, $f(n) \in U$.

tendsto_const_nhds theorem

{f : Filter α} : Tendsto (fun _ : α => x) f (𝓝 x)

Full source

theorem tendsto_const_nhds {f : Filter α} : Tendsto (fun _ : α => x) f (𝓝 x) :=
  tendsto_nhds.mpr fun _ _ ha => univ_mem' fun _ => ha

Constant Function Converges to Its Value in Neighborhood Filter

Informal description

For any filter $f$ on a type $\alpha$, the constant function that maps every element of $\alpha$ to a point $x$ in a topological space $X$ tends to the neighborhood filter $\mathcal{N}(x)$ as its argument tends to $f$.

tendsto_atTop_of_eventually_const theorem

{ι : Type*} [Preorder ι] {u : ι → X} {i₀ : ι} (h : ∀ i ≥ i₀, u i = x) : Tendsto u atTop (𝓝 x)

Full source

theorem tendsto_atTop_of_eventually_const {ι : Type*} [Preorder ι]
    {u : ι → X} {i₀ : ι} (h : ∀ i ≥ i₀, u i = x) : Tendsto u atTop (𝓝 x) :=
  Tendsto.congr' (EventuallyEq.symm ((eventually_ge_atTop i₀).mono h)) tendsto_const_nhds

Eventually Constant Function Converges to Its Value at Infinity

Informal description

Let $\iota$ be a preordered type and $X$ a topological space. For a function $u \colon \iota \to X$ and an index $i_0 \in \iota$, if $u(i) = x$ for all $i \geq i_0$, then $u$ tends to the neighborhood filter $\mathcal{N}(x)$ as the argument tends to infinity in $\iota$.

tendsto_atBot_of_eventually_const theorem

{ι : Type*} [Preorder ι] {u : ι → X} {i₀ : ι} (h : ∀ i ≤ i₀, u i = x) : Tendsto u atBot (𝓝 x)

Full source

theorem tendsto_atBot_of_eventually_const {ι : Type*} [Preorder ι]
    {u : ι → X} {i₀ : ι} (h : ∀ i ≤ i₀, u i = x) : Tendsto u atBot (𝓝 x) :=
  tendsto_atTop_of_eventually_const (ι := ιᵒᵈ) h

Eventually Constant Function Converges to Its Value at Negative Infinity

Informal description

Let $\iota$ be a preordered type and $X$ a topological space. For a function $u \colon \iota \to X$ and an index $i_0 \in \iota$, if $u(i) = x$ for all $i \leq i_0$, then $u$ tends to the neighborhood filter $\mathcal{N}(x)$ as the argument tends to negative infinity in $\iota$.

pure_le_nhds theorem

: pure ≤ (𝓝 : X → Filter X)

Full source

theorem pure_le_nhds : pure ≤ (𝓝 : X → Filter X) := fun _ _ hs => mem_pure.2 <| mem_of_mem_nhds hs

Principal Ultrafilter is Contained in Neighborhood Filter

Informal description

For any point $x$ in a topological space $X$, the pure filter (principal ultrafilter) at $x$ is contained in the neighborhood filter $\mathcal{N}(x)$ of $x$. In other words, every neighborhood of $x$ contains $x$ itself.

tendsto_pure_nhds theorem

(f : α → X) (a : α) : Tendsto f (pure a) (𝓝 (f a))

Full source

theorem tendsto_pure_nhds (f : α → X) (a : α) : Tendsto f (pure a) (𝓝 (f a)) :=
  (tendsto_pure_pure f a).mono_right (pure_le_nhds _)

Limit of Function at Point via Principal Ultrafilter

Informal description

For any function $f \colon \alpha \to X$ and any point $a \in \alpha$, the function $f$ tends to $f(a)$ with respect to the neighborhood filter $\mathcal{N}(f(a))$ when the input approaches $a$ along the principal ultrafilter at $a$.

OrderTop.tendsto_atTop_nhds theorem

[PartialOrder α] [OrderTop α] (f : α → X) : Tendsto f atTop (𝓝 (f ⊤))

Full source

theorem OrderTop.tendsto_atTop_nhds [PartialOrder α] [OrderTop α] (f : α → X) :
    Tendsto f atTop (𝓝 (f ⊤)) :=
  (tendsto_atTop_pure f).mono_right (pure_le_nhds _)

Limit at Top Element Equals Value at Top

Informal description

Let $X$ be a topological space and $\alpha$ be a partially ordered set with a greatest element $\top$. For any function $f \colon \alpha \to X$, the limit of $f$ at $\top$ (with respect to the order topology) is equal to $f(\top)$, i.e., $\lim_{x \to \top} f(x) = f(\top)$.

nhds_neBot instance

: NeBot (𝓝 x)

Full source

@[simp]
instance nhds_neBot : NeBot (𝓝 x) :=
  neBot_of_le (pure_le_nhds x)

Neighborhood Filters are Nonempty

Informal description

For any point $x$ in a topological space $X$, the neighborhood filter $\mathcal{N}(x)$ is nonempty and does not contain the empty set.

tendsto_nhds_of_eventually_eq theorem

{l : Filter α} {f : α → X} (h : ∀ᶠ x' in l, f x' = x) : Tendsto f l (𝓝 x)

Full source

theorem tendsto_nhds_of_eventually_eq {l : Filter α} {f : α → X} (h : ∀ᶠ x' in l, f x' = x) :
    Tendsto f l (𝓝 x) :=
  tendsto_const_nhds.congr' (.symm h)

Limit of Eventually Constant Function is Constant

Informal description

Let $X$ be a topological space, $\alpha$ a type, and $l$ a filter on $\alpha$. For any function $f \colon \alpha \to X$ and any point $x \in X$, if $f(x') = x$ for all $x'$ in $l$ eventually (i.e., for all $x'$ in some set belonging to $l$), then $f$ tends to $x$ along the filter $l$.

Filter.EventuallyEq.tendsto theorem

{l : Filter α} {f : α → X} (hf : f =ᶠ[l] fun _ ↦ x) : Tendsto f l (𝓝 x)

Full source

theorem Filter.EventuallyEq.tendsto {l : Filter α} {f : α → X} (hf : f =ᶠ[l] fun _ ↦ x) :
    Tendsto f l (𝓝 x) :=
  tendsto_nhds_of_eventually_eq hf

Limit of Eventually Constant Function is Constant

Informal description

Let $X$ be a topological space, $\alpha$ a type, and $l$ a filter on $\alpha$. For any function $f \colon \alpha \to X$ and any point $x \in X$, if $f$ is eventually equal to the constant function $\lambda \_, x$ along $l$, then $f$ tends to $x$ along the filter $l$.

interior_eq_nhds' theorem

: interior s = {x | s ∈ 𝓝 x}

Full source

theorem interior_eq_nhds' : interior s = { x | s ∈ 𝓝 x } :=
  Set.ext fun x => by simp only [mem_interior, mem_nhds_iff, mem_setOf_eq]

Interior as Points with Set in Neighborhood Filter

Informal description

The interior of a set $s$ in a topological space is equal to the set of all points $x$ for which $s$ is a neighborhood of $x$, i.e., \[ \text{interior}(s) = \{x \mid s \in \mathcal{N}(x)\}, \] where $\mathcal{N}(x)$ denotes the neighborhood filter at $x$.

interior_eq_nhds theorem

: interior s = {x | 𝓝 x ≤ 𝓟 s}

Full source

theorem interior_eq_nhds : interior s = { x | 𝓝 x ≤ 𝓟 s } :=
  interior_eq_nhds'.trans <| by simp only [le_principal_iff]

Interior as Points with Neighborhood Filter Contained in Principal Filter

Informal description

The interior of a set $s$ in a topological space is equal to the set of all points $x$ for which the neighborhood filter $\mathcal{N}(x)$ is contained in the principal filter generated by $s$, i.e., \[ \text{interior}(s) = \{x \mid \mathcal{N}(x) \subseteq \mathcal{P}(s)\}, \] where $\mathcal{P}(s)$ denotes the principal filter of $s$.

interior_mem_nhds theorem

: interior s ∈ 𝓝 x ↔ s ∈ 𝓝 x

Full source

@[simp]
theorem interior_mem_nhds : interiorinterior s ∈ 𝓝 xinterior s ∈ 𝓝 x ↔ s ∈ 𝓝 x :=
  ⟨fun h => mem_of_superset h interior_subset, fun h =>
    IsOpen.mem_nhds isOpen_interior (mem_interior_iff_mem_nhds.2 h)⟩

Equivalence of Interior and Set in Neighborhood Filter

Informal description

For any set $s$ in a topological space and any point $x$, the interior of $s$ is a neighborhood of $x$ if and only if $s$ itself is a neighborhood of $x$. In other words: \[ \text{interior}(s) \in \mathcal{N}(x) \leftrightarrow s \in \mathcal{N}(x), \] where $\mathcal{N}(x)$ denotes the neighborhood filter at $x$.

interior_setOf_eq theorem

{p : X → Prop} : interior {x | p x} = {x | ∀ᶠ y in 𝓝 x, p y}

Full source

theorem interior_setOf_eq {p : X → Prop} : interior { x | p x } = { x | ∀ᶠ y in 𝓝 x, p y } :=
  interior_eq_nhds'

Interior of a Predicate Set via Neighborhoods

Informal description

For any predicate $p : X \to \text{Prop}$ on a topological space $X$, the interior of the set $\{x \mid p(x)\}$ is equal to the set of points $x$ for which $p(y)$ holds for all $y$ in some neighborhood of $x$. That is, \[ \text{interior}\{x \mid p(x)\} = \{x \mid \forall y \in \mathcal{N}(x), p(y)\}, \] where $\mathcal{N}(x)$ denotes the neighborhood filter at $x$.

isOpen_setOf_eventually_nhds theorem

{p : X → Prop} : IsOpen {x | ∀ᶠ y in 𝓝 x, p y}

Full source

theorem isOpen_setOf_eventually_nhds {p : X → Prop} : IsOpen { x | ∀ᶠ y in 𝓝 x, p y } := by
  simp only [← interior_setOf_eq, isOpen_interior]

Openness of the Set Where a Predicate Holds Eventually in Neighborhoods

Informal description

For any predicate $p : X \to \text{Prop}$, the set $\{x \mid \text{for all } y \text{ in a neighborhood of } x, p(y)\}$ is open in the topological space $X$.

subset_interior_iff_nhds theorem

{V : Set X} : s ⊆ interior V ↔ ∀ x ∈ s, V ∈ 𝓝 x

Full source

theorem subset_interior_iff_nhds {V : Set X} : s ⊆ interior Vs ⊆ interior V ↔ ∀ x ∈ s, V ∈ 𝓝 x := by
  simp_rw [subset_def, mem_interior_iff_mem_nhds]

Subset of Interior Equivalently Characterized by Neighborhood Condition

Informal description

For any subset $s$ of a topological space $X$ and any subset $V \subseteq X$, $s$ is contained in the interior of $V$ if and only if for every point $x \in s$, $V$ is a neighborhood of $x$.

isOpen_iff_nhds theorem

: IsOpen s ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s

Full source

theorem isOpen_iff_nhds : IsOpenIsOpen s ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s :=
  calc
    IsOpen s ↔ s ⊆ interior s := subset_interior_iff_isOpen.symm
    _ ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s := by simp_rw [interior_eq_nhds, subset_def, mem_setOf]

Open Set Characterization via Neighborhood Filters

Informal description

A subset $s$ of a topological space $X$ is open if and only if for every point $x \in s$, the neighborhood filter $\mathcal{N}(x)$ is contained in the principal filter generated by $s$, i.e., \[ \text{IsOpen}(s) \leftrightarrow \forall x \in s, \mathcal{N}(x) \subseteq \mathcal{P}(s). \]

TopologicalSpace.ext_iff_nhds theorem

{X} {t t' : TopologicalSpace X} : t = t' ↔ ∀ x, @nhds _ t x = @nhds _ t' x

Full source

theorem TopologicalSpace.ext_iff_nhds {X} {t t' : TopologicalSpace X} :
    t = t' ↔ ∀ x, @nhds _ t x = @nhds _ t' x :=
  ⟨fun H _ ↦ congrFun (congrArg _ H) _, fun H ↦ by ext; simp_rw [@isOpen_iff_nhds _ _ _, H]⟩

Equality of Topological Spaces via Neighborhood Filters

Informal description

Two topological space structures $t$ and $t'$ on a set $X$ are equal if and only if for every point $x \in X$, the neighborhood filters $\mathcal{N}_t(x)$ and $\mathcal{N}_{t'}(x)$ coincide.

isOpen_iff_mem_nhds theorem

: IsOpen s ↔ ∀ x ∈ s, s ∈ 𝓝 x

Full source

theorem isOpen_iff_mem_nhds : IsOpenIsOpen s ↔ ∀ x ∈ s, s ∈ 𝓝 x :=
  isOpen_iff_nhds.trans <| forall_congr' fun _ => imp_congr_right fun _ => le_principal_iff

Open Set Characterization via Membership in Neighborhood Filters

Informal description

A subset $s$ of a topological space $X$ is open if and only if for every point $x \in s$, the set $s$ belongs to the neighborhood filter $\mathcal{N}(x)$ of $x$.

isOpen_iff_eventually theorem

: IsOpen s ↔ ∀ x, x ∈ s → ∀ᶠ y in 𝓝 x, y ∈ s

Full source

/-- A set `s` is open iff for every point `x` in `s` and every `y` close to `x`, `y` is in `s`. -/
theorem isOpen_iff_eventually : IsOpenIsOpen s ↔ ∀ x, x ∈ s → ∀ᶠ y in 𝓝 x, y ∈ s :=
  isOpen_iff_mem_nhds

Open Set Characterization via Eventual Membership in Neighborhoods

Informal description

A subset $s$ of a topological space $X$ is open if and only if for every point $x \in s$, the neighborhood filter $\mathcal{N}(x)$ eventually contains all points $y$ that belong to $s$.

isOpen_singleton_iff_nhds_eq_pure theorem

(x : X) : IsOpen ({ x } : Set X) ↔ 𝓝 x = pure x

Full source

theorem isOpen_singleton_iff_nhds_eq_pure (x : X) : IsOpenIsOpen ({x} : Set X) ↔ 𝓝 x = pure x := by
  simp [← (pure_le_nhds _).le_iff_eq, isOpen_iff_mem_nhds]

Singleton Openness Criterion via Neighborhood Filter Equality

Informal description

For a point $x$ in a topological space $X$, the singleton set $\{x\}$ is open if and only if the neighborhood filter $\mathcal{N}(x)$ is equal to the principal ultrafilter at $x$.

isOpen_singleton_iff_punctured_nhds theorem

(x : X) : IsOpen ({ x } : Set X) ↔ 𝓝[≠] x = ⊥

Full source

theorem isOpen_singleton_iff_punctured_nhds (x : X) : IsOpenIsOpen ({x} : Set X) ↔ 𝓝[≠] x = ⊥ := by
  rw [isOpen_singleton_iff_nhds_eq_pure, nhdsWithin, ← mem_iff_inf_principal_compl,
      le_antisymm_iff]
  simp [pure_le_nhds x]

Singleton Openness Criterion via Punctured Neighborhood Filter Triviality

Informal description

For a point $x$ in a topological space $X$, the singleton set $\{x\}$ is open if and only if the punctured neighborhood filter $\mathcal{N}_\neq(x)$ (the filter of neighborhoods of $x$ excluding $x$ itself) is equal to the bottom filter $\bot$.

mem_closure_iff_frequently theorem

: x ∈ closure s ↔ ∃ᶠ x in 𝓝 x, x ∈ s

Full source

theorem mem_closure_iff_frequently : x ∈ closure sx ∈ closure s ↔ ∃ᶠ x in 𝓝 x, x ∈ s := by
  rw [Filter.Frequently, Filter.Eventually, ← mem_interior_iff_mem_nhds,
    closure_eq_compl_interior_compl, mem_compl_iff, compl_def]

Characterization of Closure via Cluster Points: $x \in \overline{s} \leftrightarrow s$ is frequently in $\mathcal{N}(x)$

Informal description

A point $x$ belongs to the closure of a set $s$ in a topological space if and only if $x$ is a cluster point of $s$ with respect to the neighborhood filter $\mathcal{N}(x)$, meaning that $s$ intersects every neighborhood of $x$ frequently (i.e., for every neighborhood $U$ of $x$, there exists a point $y \in U$ such that $y \in s$).

isClosed_iff_frequently theorem

: IsClosed s ↔ ∀ x, (∃ᶠ y in 𝓝 x, y ∈ s) → x ∈ s

Full source

/-- A set `s` is closed iff for every point `x`, if there is a point `y` close to `x` that belongs
to `s` then `x` is in `s`. -/
theorem isClosed_iff_frequently : IsClosedIsClosed s ↔ ∀ x, (∃ᶠ y in 𝓝 x, y ∈ s) → x ∈ s := by
  rw [← closure_subset_iff_isClosed]
  refine forall_congr' fun x => ?_
  rw [mem_closure_iff_frequently]

Characterization of Closed Sets via Cluster Points

Informal description

A subset $s$ of a topological space is closed if and only if for every point $x$, if there exists a point $y$ in every neighborhood of $x$ such that $y \in s$, then $x \in s$.

nhdsWithin_neBot theorem

: (𝓝[s] x).NeBot ↔ ∀ ⦃t⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty

Full source

lemma nhdsWithin_neBot : (𝓝[s] x).NeBot ↔ ∀ ⦃t⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty := by
  rw [nhdsWithin, inf_neBot_iff]
  exact forall₂_congr fun U _ ↦
    ⟨fun h ↦ h (mem_principal_self _), fun h u hsu ↦ h.mono <| inter_subset_inter_right _ hsu⟩

Nonempty Neighborhood Filter Within a Subset Characterized by Nonempty Intersections

Informal description

The neighborhood filter of a point $x$ within a subset $s$ of a topological space is nonempty if and only if for every neighborhood $t$ of $x$, the intersection $t \cap s$ is nonempty.

nhdsWithin_mono theorem

(x : X) {s t : Set X} (h : s ⊆ t) : 𝓝[s] x ≤ 𝓝[t] x

Full source

@[gcongr]
theorem nhdsWithin_mono (x : X) {s t : Set X} (h : s ⊆ t) : 𝓝[s] x ≤ 𝓝[t] x :=
  inf_le_inf_left _ (principal_mono.mpr h)

Monotonicity of Neighborhood Filters with Respect to Subset Inclusion

Informal description

For any point $x$ in a topological space $X$ and any subsets $s, t \subseteq X$ with $s \subseteq t$, the neighborhood filter of $x$ within $s$ is less than or equal to the neighborhood filter of $x$ within $t$, i.e., $\mathcal{N}_s(x) \leq \mathcal{N}_t(x)$.

IsClosed.interior_union_left theorem

(_ : IsClosed s) : interior (s ∪ t) ⊆ s ∪ interior t

Full source

theorem IsClosed.interior_union_left (_ : IsClosed s) :
    interiorinterior (s ∪ t) ⊆ s ∪ interior t := fun a ⟨u, ⟨⟨hu₁, hu₂⟩, ha⟩⟩ =>
  (Classical.em (a ∈ s)).imp_right fun h =>
    mem_interior.mpr
      ⟨u ∩ sᶜ, fun _x hx => (hu₂ hx.1).resolve_left hx.2, IsOpen.inter hu₁ IsClosed.isOpen_compl,
        ⟨ha, h⟩⟩

Interior of Union with Closed Set is Contained in Union with Interior

Informal description

For any closed set $s$ and any set $t$ in a topological space, the interior of the union $s \cup t$ is contained in the union of $s$ and the interior of $t$, i.e., $\text{interior}(s \cup t) \subseteq s \cup \text{interior}(t)$.

IsClosed.interior_union_right theorem

(h : IsClosed t) : interior (s ∪ t) ⊆ interior s ∪ t

Full source

theorem IsClosed.interior_union_right (h : IsClosed t) :
    interiorinterior (s ∪ t) ⊆ interior s ∪ t := by
  simpa only [union_comm _ t] using h.interior_union_left

Interior of Union with Closed Set is Contained in Interior Union with Closed Set

Informal description

For any closed set $t$ and any set $s$ in a topological space, the interior of the union $s \cup t$ is contained in the union of the interior of $s$ and $t$, i.e., $\text{interior}(s \cup t) \subseteq \text{interior}(s) \cup t$.

IsOpen.inter_closure theorem

(h : IsOpen s) : s ∩ closure t ⊆ closure (s ∩ t)

Full source

theorem IsOpen.inter_closure (h : IsOpen s) : s ∩ closure ts ∩ closure t ⊆ closure (s ∩ t) :=
  compl_subset_compl.mp <| by
    simpa only [← interior_compl, compl_inter] using IsClosed.interior_union_left h.isClosed_compl

Open Set Intersection with Closure is Contained in Closure of Intersection

Informal description

For any open set $s$ and any set $t$ in a topological space, the intersection of $s$ with the closure of $t$ is contained in the closure of the intersection of $s$ and $t$, i.e., $s \cap \overline{t} \subseteq \overline{s \cap t}$.

IsOpen.closure_inter theorem

(h : IsOpen t) : closure s ∩ t ⊆ closure (s ∩ t)

Full source

theorem IsOpen.closure_inter (h : IsOpen t) : closureclosure s ∩ tclosure s ∩ t ⊆ closure (s ∩ t) := by
  simpa only [inter_comm t] using h.inter_closure

Open Set Intersection with Closure is Contained in Closure of Intersection (Symmetric Version)

Informal description

For any open set $t$ and any set $s$ in a topological space, the intersection of the closure of $s$ with $t$ is contained in the closure of the intersection of $s$ and $t$, i.e., $\overline{s} \cap t \subseteq \overline{s \cap t}$.

Dense.open_subset_closure_inter theorem

(hs : Dense s) (ht : IsOpen t) : t ⊆ closure (t ∩ s)

Full source

theorem Dense.open_subset_closure_inter (hs : Dense s) (ht : IsOpen t) :
    t ⊆ closure (t ∩ s) :=
  calc
    t = t ∩ closure s := by rw [hs.closure_eq, inter_univ]
    _ ⊆ closure (t ∩ s) := ht.inter_closure

Open Subset Contained in Closure of Intersection with Dense Set

Informal description

For any dense subset $s$ and any open subset $t$ in a topological space, $t$ is contained in the closure of the intersection of $t$ and $s$, i.e., $t \subseteq \overline{t \cap s}$.

Dense.inter_of_isOpen_left theorem

(hs : Dense s) (ht : Dense t) (hso : IsOpen s) : Dense (s ∩ t)

Full source

/-- The intersection of an open dense set with a dense set is a dense set. -/
theorem Dense.inter_of_isOpen_left (hs : Dense s) (ht : Dense t) (hso : IsOpen s) :
    Dense (s ∩ t) := fun x =>
  closure_minimal hso.inter_closure isClosed_closure <| by simp [hs.closure_eq, ht.closure_eq]

Intersection of Open Dense Set with Dense Set is Dense

Informal description

Let $s$ and $t$ be dense subsets of a topological space, with $s$ open. Then the intersection $s \cap t$ is also dense.

Dense.inter_of_isOpen_right theorem

(hs : Dense s) (ht : Dense t) (hto : IsOpen t) : Dense (s ∩ t)

Full source

/-- The intersection of a dense set with an open dense set is a dense set. -/
theorem Dense.inter_of_isOpen_right (hs : Dense s) (ht : Dense t) (hto : IsOpen t) :
    Dense (s ∩ t) :=
  inter_comm t s ▸ ht.inter_of_isOpen_left hs hto

Density of Intersection with Open Dense Set (Right Version)

Informal description

Let $s$ and $t$ be dense subsets of a topological space, with $t$ open. Then the intersection $s \cap t$ is also dense.

Dense.inter_nhds_nonempty theorem

(hs : Dense s) (ht : t ∈ 𝓝 x) : (s ∩ t).Nonempty

Full source

theorem Dense.inter_nhds_nonempty (hs : Dense s) (ht : t ∈ 𝓝 x) :
    (s ∩ t).Nonempty :=
  let ⟨U, hsub, ho, hx⟩ := mem_nhds_iff.1 ht
  (hs.inter_open_nonempty U ho ⟨x, hx⟩).mono fun _y hy => ⟨hy.2, hsub hy.1⟩

Nonempty Intersection of Dense Set with Neighborhood

Informal description

For a dense subset $s$ of a topological space and any neighborhood $t$ of a point $x$, the intersection $s \cap t$ is nonempty.

closure_diff theorem

: closure s \ closure t ⊆ closure (s \ t)

Full source

theorem closure_diff : closureclosure s \ closure tclosure s \ closure t ⊆ closure (s \ t) :=
  calc
    closure s \ closure t = (closure t)ᶜ ∩ closure s := by simp only [diff_eq, inter_comm]
    _ ⊆ closure ((closure t)ᶜ ∩ s)calc
    closure s \ closure t = (closure t)ᶜ ∩ closure s := by simp only [diff_eq, inter_comm]
    _ ⊆ closure ((closure t)ᶜ ∩ s) := (isOpen_compl_iff.mpr <| isClosed_closure).inter_closure
    _ = closure (s \ closure t) := by simp only [diff_eq, inter_comm]
    _ ⊆ closure (s \ t) := closure_mono <| diff_subset_diff (Subset.refl s) subset_closure

Closure of Set Difference is Contained in Difference of Closures

Informal description

For any subsets $s$ and $t$ of a topological space, the set difference between the closure of $s$ and the closure of $t$ is contained in the closure of the set difference between $s$ and $t$, i.e., $\overline{s} \setminus \overline{t} \subseteq \overline{s \setminus t}$.

Filter.Frequently.mem_of_closed theorem

(h : ∃ᶠ x in 𝓝 x, x ∈ s) (hs : IsClosed s) : x ∈ s

Full source

theorem Filter.Frequently.mem_of_closed (h : ∃ᶠ x in 𝓝 x, x ∈ s)
    (hs : IsClosed s) : x ∈ s :=
  hs.closure_subset h.mem_closure

Frequent Membership in Closed Set Implies Membership

Informal description

If a point $x$ in a topological space has the property that there exists a neighborhood filter $\mathcal{N}(x)$ such that $x$ is frequently in a closed set $s$ (i.e., $x \in s$ for infinitely many points in any neighborhood of $x$), then $x$ must belong to $s$.

IsClosed.mem_of_frequently_of_tendsto theorem

{f : α → X} {b : Filter α} (hs : IsClosed s) (h : ∃ᶠ x in b, f x ∈ s) (hf : Tendsto f b (𝓝 x)) : x ∈ s

Full source

theorem IsClosed.mem_of_frequently_of_tendsto {f : α → X} {b : Filter α}
    (hs : IsClosed s) (h : ∃ᶠ x in b, f x ∈ s) (hf : Tendsto f b (𝓝 x)) : x ∈ s :=
  (hf.frequently <| show ∃ᶠ x in b, (fun y => y ∈ s) (f x) from h).mem_of_closed hs

Closed Set Membership via Frequent Convergence

Informal description

Let $X$ be a topological space, $s \subseteq X$ a closed subset, and $x \in X$ a point. Given a function $f : \alpha \to X$ and a filter $b$ on $\alpha$, if: 1. $f(x) \in s$ frequently along $b$ (i.e., for every set in $b$, there exists $x$ in that set with $f(x) \in s$), and 2. $f$ tends to $x$ along $b$ with respect to the neighborhood filter $\mathcal{N}(x)$, then $x$ belongs to $s$.

IsClosed.mem_of_tendsto theorem

 {f : α → X} {b : Filter α} [NeBot b] (hs : IsClosed s) (hf : Tendsto f b (𝓝 x)) (h : ∀ᶠ x in b, f x ∈ s) : x ∈ s

Full source

theorem IsClosed.mem_of_tendsto {f : α → X} {b : Filter α} [NeBot b]
    (hs : IsClosed s) (hf : Tendsto f b (𝓝 x)) (h : ∀ᶠ x in b, f x ∈ s) : x ∈ s :=
  hs.mem_of_frequently_of_tendsto h.frequently hf

Closed Set Membership via Filter Convergence

Informal description

Let $X$ be a topological space, $s \subseteq X$ a closed subset, and $x \in X$ a point. Given a function $f : \alpha \to X$ and a non-trivial filter $b$ on $\alpha$, if: 1. $f$ tends to $x$ along $b$ with respect to the neighborhood filter $\mathcal{N}(x)$, and 2. $f(x) \in s$ eventually along $b$ (i.e., there exists a set in $b$ where $f(x) \in s$ for all $x$ in that set), then $x$ belongs to $s$.

mem_closure_of_frequently_of_tendsto theorem

{f : α → X} {b : Filter α} (h : ∃ᶠ x in b, f x ∈ s) (hf : Tendsto f b (𝓝 x)) : x ∈ closure s

Full source

theorem mem_closure_of_frequently_of_tendsto {f : α → X} {b : Filter α}
    (h : ∃ᶠ x in b, f x ∈ s) (hf : Tendsto f b (𝓝 x)) : x ∈ closure s :=
  (hf.frequently h).mem_closure

Closure Membership via Frequent Convergence

Informal description

Let $X$ be a topological space, $s \subseteq X$ a subset, and $x \in X$ a point. If there exists a filter $b$ on some type $\alpha$ and a function $f : \alpha \to X$ such that: 1. $f(x) \in s$ frequently along $b$ (i.e., for every set in $b$, there exists $x$ in that set with $f(x) \in s$), and 2. $f$ tends to $x$ along $b$ with respect to the neighborhood filter $\mathcal{N}(x)$, then $x$ belongs to the closure of $s$.

mem_closure_of_tendsto theorem

{f : α → X} {b : Filter α} [NeBot b] (hf : Tendsto f b (𝓝 x)) (h : ∀ᶠ x in b, f x ∈ s) : x ∈ closure s

Full source

theorem mem_closure_of_tendsto {f : α → X} {b : Filter α} [NeBot b]
    (hf : Tendsto f b (𝓝 x)) (h : ∀ᶠ x in b, f x ∈ s) : x ∈ closure s :=
  mem_closure_of_frequently_of_tendsto h.frequently hf

Closure Membership via Filter Convergence

Informal description

Let $X$ be a topological space, $s \subseteq X$ a subset, and $x \in X$ a point. Given a non-trivial filter $b$ on some type $\alpha$ and a function $f : \alpha \to X$ such that: 1. $f$ tends to $x$ along $b$ with respect to the neighborhood filter $\mathcal{N}(x)$, and 2. $f(x) \in s$ eventually along $b$ (i.e., there exists a set in $b$ where $f(x) \in s$ for all $x$ in that set), then $x$ belongs to the closure of $s$.

tendsto_inf_principal_nhds_iff_of_forall_eq theorem

 {f : α → X} {l : Filter α} {s : Set α} (h : ∀ a ∉ s, f a = x) : Tendsto f (l ⊓ 𝓟 s) (𝓝 x) ↔ Tendsto f l (𝓝 x)

Full source

/-- Suppose that `f` sends the complement to `s` to a single point `x`, and `l` is some filter.
Then `f` tends to `x` along `l` restricted to `s` if and only if it tends to `x` along `l`. -/
theorem tendsto_inf_principal_nhds_iff_of_forall_eq {f : α → X} {l : Filter α} {s : Set α}
    (h : ∀ a ∉ s, f a = x) : TendstoTendsto f (l ⊓ 𝓟 s) (𝓝 x) ↔ Tendsto f l (𝓝 x) := by
  rw [tendsto_iff_comap, tendsto_iff_comap]
  replace h : 𝓟 sᶜ ≤ comap f (𝓝 x) := by
    rintro U ⟨t, ht, htU⟩ x hx
    have : f x ∈ t := (h x hx).symm ▸ mem_of_mem_nhds ht
    exact htU this
  refine ⟨fun h' => ?_, le_trans inf_le_left⟩
  have := sup_le h' h
  rw [sup_inf_right, sup_principal, union_compl_self, principal_univ, inf_top_eq, sup_le_iff]
    at this
  exact this.1

Equivalence of Filter Convergence When Function is Constant Outside a Set

Informal description

Let $f : \alpha \to X$ be a function, $l$ a filter on $\alpha$, and $s \subseteq \alpha$ a subset such that $f(a) = x$ for all $a \notin s$. Then the following are equivalent: 1. $f$ tends to $x$ along the filter $l \sqcap \mathcal{P}(s)$ (the restriction of $l$ to $s$) 2. $f$ tends to $x$ along $l$.

Tags