Mathlib.Topology.NhdsSet

nhdsSet_diagonal theorem

(X) [TopologicalSpace (X × X)] : 𝓝ˢ (diagonal X) = ⨆ (x : X), 𝓝 (x, x)

Full source

theorem nhdsSet_diagonal (X) [TopologicalSpace (X × X)] :
    𝓝ˢ (diagonal X) = ⨆ (x : X), 𝓝 (x, x) := by
  rw [nhdsSet, ← range_diag, ← range_comp]
  rfl

Neighborhood Filter of Diagonal Equals Supremum of Point Neighborhoods

Informal description

For any topological space $X \times X$, the neighborhood filter of the diagonal set $\Delta_X = \{(x,x) \mid x \in X\}$ is equal to the supremum of the neighborhood filters at each point $(x,x)$ on the diagonal, i.e., \[ \mathcal{N}(\Delta_X) = \bigsqcup_{x \in X} \mathcal{N}(x,x). \]

mem_nhdsSet_iff_forall theorem

: s ∈ 𝓝ˢ t ↔ ∀ x : X, x ∈ t → s ∈ 𝓝 x

Full source

theorem mem_nhdsSet_iff_forall : s ∈ 𝓝ˢ ts ∈ 𝓝ˢ t ↔ ∀ x : X, x ∈ t → s ∈ 𝓝 x := by
  simp_rw [nhdsSet, Filter.mem_sSup, forall_mem_image]

Characterization of Neighborhood Filter Membership via Pointwise Neighborhoods

Informal description

A set $s$ is in the neighborhood filter $\mathcal{N}(t)$ of a set $t$ if and only if for every point $x \in t$, the set $s$ is a neighborhood of $x$.

nhdsSet_le theorem

: 𝓝ˢ s ≤ f ↔ ∀ x ∈ s, 𝓝 x ≤ f

Full source

lemma nhdsSet_le : 𝓝ˢ𝓝ˢ s ≤ f ↔ ∀ x ∈ s, 𝓝 x ≤ f := by simp [nhdsSet]

Comparison of Neighborhood Filter with Pointwise Filters: $\mathcal{N}^s(s) \leq f \leftrightarrow \forall x \in s, \mathcal{N}(x) \leq f$

Informal description

The neighborhood filter $\mathcal{N}^s(s)$ of a set $s$ is less than or equal to a filter $f$ if and only if for every point $x \in s$, the neighborhood filter $\mathcal{N}(x)$ at $x$ is less than or equal to $f$.

bUnion_mem_nhdsSet theorem

{t : X → Set X} (h : ∀ x ∈ s, t x ∈ 𝓝 x) : (⋃ x ∈ s, t x) ∈ 𝓝ˢ s

Full source

theorem bUnion_mem_nhdsSet {t : X → Set X} (h : ∀ x ∈ s, t x ∈ 𝓝 x) : (⋃ x ∈ s, t x) ∈ 𝓝ˢ s :=
  mem_nhdsSet_iff_forall.2 fun x hx => mem_of_superset (h x hx) <|
    subset_iUnion₂ (s := fun x _ => t x) x hx

Union of Pointwise Neighborhoods is a Set Neighborhood

Informal description

Let $X$ be a topological space and $s \subseteq X$ a subset. For a family of sets $\{t(x)\}_{x \in s}$ such that for each $x \in s$, $t(x)$ is a neighborhood of $x$, then the union $\bigcup_{x \in s} t(x)$ is a neighborhood of the set $s$.

subset_interior_iff_mem_nhdsSet theorem

: s ⊆ interior t ↔ t ∈ 𝓝ˢ s

Full source

theorem subset_interior_iff_mem_nhdsSet : s ⊆ interior ts ⊆ interior t ↔ t ∈ 𝓝ˢ s := by
  simp_rw [mem_nhdsSet_iff_forall, subset_interior_iff_nhds]

Interior Subset iff Neighborhood Condition

Informal description

A set $s$ is contained in the interior of a set $t$ if and only if $t$ is a neighborhood of $s$ (i.e., $t$ belongs to the neighborhood filter $\mathcal{N}^s(s)$ of $s$).

disjoint_principal_nhdsSet theorem

: Disjoint (𝓟 s) (𝓝ˢ t) ↔ Disjoint (closure s) t

Full source

theorem disjoint_principal_nhdsSet : DisjointDisjoint (𝓟 s) (𝓝ˢ t) ↔ Disjoint (closure s) t := by
  rw [disjoint_principal_left, ← subset_interior_iff_mem_nhdsSet, interior_compl,
    subset_compl_iff_disjoint_left]

Disjointness of Principal and Neighborhood Filters ↔ Disjointness of Closure and Set

Informal description

The principal filter $\mathcal{P}(s)$ and the neighborhood filter $\mathcal{N}^s(t)$ are disjoint if and only if the closure of $s$ is disjoint from $t$, i.e., $\text{Disjoint}(\mathcal{P}(s), \mathcal{N}^s(t)) \leftrightarrow \text{Disjoint}(\overline{s}, t)$.

disjoint_nhdsSet_principal theorem

: Disjoint (𝓝ˢ s) (𝓟 t) ↔ Disjoint s (closure t)

Full source

theorem disjoint_nhdsSet_principal : DisjointDisjoint (𝓝ˢ s) (𝓟 t) ↔ Disjoint s (closure t) := by
  rw [disjoint_comm, disjoint_principal_nhdsSet, disjoint_comm]

Disjointness of Neighborhood and Principal Filters ↔ Disjointness of Set and Closure

Informal description

The neighborhood filter $\mathcal{N}^s(s)$ of a set $s$ and the principal filter $\mathcal{P}(t)$ are disjoint if and only if $s$ is disjoint from the closure of $t$, i.e., $\text{Disjoint}(\mathcal{N}^s(s), \mathcal{P}(t)) \leftrightarrow \text{Disjoint}(s, \overline{t})$.

mem_nhdsSet_iff_exists theorem

: s ∈ 𝓝ˢ t ↔ ∃ U : Set X, IsOpen U ∧ t ⊆ U ∧ U ⊆ s

Full source

theorem mem_nhdsSet_iff_exists : s ∈ 𝓝ˢ ts ∈ 𝓝ˢ t ↔ ∃ U : Set X, IsOpen U ∧ t ⊆ U ∧ U ⊆ s := by
  rw [← subset_interior_iff_mem_nhdsSet, subset_interior_iff]

Existence of Open Set in Neighborhood Filter

Informal description

A set $s$ belongs to the neighborhood filter $\mathcal{N}^s(t)$ of a set $t$ if and only if there exists an open set $U$ such that $t \subseteq U$ and $U \subseteq s$.

eventually_nhdsSet_iff_exists theorem

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

Full source

/-- A proposition is true on a set neighborhood of `s` iff it is true on a larger open set -/
theorem eventually_nhdsSet_iff_exists {p : X → Prop} :
    (∀ᶠ x in 𝓝ˢ s, p x) ↔ ∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x, x ∈ t → p x :=
  mem_nhdsSet_iff_exists

Characterization of Eventual Truth via Open Superset

Informal description

For any predicate $p$ on a topological space $X$ and any subset $s \subseteq X$, the following are equivalent: 1. The predicate $p$ holds for all points in some neighborhood of $s$ (i.e., $\forallᶠ x \text{ in } \mathcal{N}^s(s), p(x)$). 2. There exists an open set $t$ containing $s$ such that $p(x)$ holds for all $x \in t$. In other words, $p$ is eventually true in the neighborhood filter of $s$ if and only if there's an open superset of $s$ where $p$ holds everywhere.

eventually_nhdsSet_iff_forall theorem

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

Full source

/-- A proposition is true on a set neighborhood of `s`
iff it is eventually true near each point in the set. -/
theorem eventually_nhdsSet_iff_forall {p : X → Prop} :
    (∀ᶠ x in 𝓝ˢ s, p x) ↔ ∀ x, x ∈ s → ∀ᶠ y in 𝓝 x, p y :=
  mem_nhdsSet_iff_forall

Characterization of Eventual Truth in Neighborhood Filter via Pointwise Neighborhoods

Informal description

For any predicate $p$ on a topological space $X$ and any subset $s \subseteq X$, the proposition $p$ holds eventually in the neighborhood filter $\mathcal{N}(s)$ of $s$ if and only if for every point $x \in s$, the proposition $p$ holds eventually in the neighborhood filter $\mathcal{N}(x)$ of $x$.

hasBasis_nhdsSet theorem

(s : Set X) : (𝓝ˢ s).HasBasis (fun U => IsOpen U ∧ s ⊆ U) fun U => U

Full source

theorem hasBasis_nhdsSet (s : Set X) : (𝓝ˢ s).HasBasis (fun U => IsOpenIsOpen U ∧ s ⊆ U) fun U => U :=
  ⟨fun t => by simp [mem_nhdsSet_iff_exists, and_assoc]⟩

Basis for Neighborhood Filter of a Set

Informal description

For any subset $s$ of a topological space $X$, the neighborhood filter $\mathcal{N}(s)$ has a basis consisting of all open sets $U$ that contain $s$, where the basis is indexed by such open sets $U$ and maps each $U$ to itself.

lift'_nhdsSet_interior theorem

(s : Set X) : (𝓝ˢ s).lift' interior = 𝓝ˢ s

Full source

@[simp]
lemma lift'_nhdsSet_interior (s : Set X) : (𝓝ˢ s).lift' interior = 𝓝ˢ s :=
  (hasBasis_nhdsSet s).lift'_interior_eq_self fun _ ↦ And.left

Neighborhood Filter Lift of Interior Equals Itself

Informal description

For any subset $s$ of a topological space $X$, the filter $\mathcal{N}(s)$ of neighborhoods of $s$ satisfies $\mathcal{N}(s).\text{lift}'(\text{interior}) = \mathcal{N}(s)$, where $\text{lift}'$ denotes the filter lift operation and $\text{interior}$ is the interior operator.

Filter.HasBasis.nhdsSet_interior theorem

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

Full source

lemma Filter.HasBasis.nhdsSet_interior {ι : Sort*} {p : ι → Prop} {s : ι → Set X} {t : Set X}
    (h : (𝓝ˢ t).HasBasis p s) : (𝓝ˢ t).HasBasis p (interior <| s ·) :=
  lift'_nhdsSet_interior t ▸ h.lift'_interior

Basis for Neighborhood Filter via Interiors

Informal description

Let $X$ be a topological space and $t \subseteq X$. Suppose the neighborhood filter $\mathcal{N}(t)$ has a basis indexed by a type $\iota$ with property $p$, where each basis element is a set $s_i$ for $i \in \iota$. Then $\mathcal{N}(t)$ also has a basis with the same index type $\iota$ and property $p$, but with basis elements given by the interiors of the original basis sets $\text{interior}(s_i)$.

IsOpen.mem_nhdsSet theorem

(hU : IsOpen s) : s ∈ 𝓝ˢ t ↔ t ⊆ s

Full source

theorem IsOpen.mem_nhdsSet (hU : IsOpen s) : s ∈ 𝓝ˢ ts ∈ 𝓝ˢ t ↔ t ⊆ s := by
  rw [← subset_interior_iff_mem_nhdsSet, hU.interior_eq]

Open Set is Neighborhood of Subset

Informal description

For an open set $s$ in a topological space, $s$ is a neighborhood of a set $t$ (i.e., $s \in \mathcal{N}^s(t)$) if and only if $t$ is a subset of $s$.

IsOpen.mem_nhdsSet_self theorem

(ho : IsOpen s) : s ∈ 𝓝ˢ s

Full source

/-- An open set belongs to its own set neighborhoods filter. -/
theorem IsOpen.mem_nhdsSet_self (ho : IsOpen s) : s ∈ 𝓝ˢ s := ho.mem_nhdsSet.mpr Subset.rfl

Open Set is Neighborhood of Itself

Informal description

For any open set $s$ in a topological space, $s$ belongs to its own neighborhood filter, i.e., $s \in \mathcal{N}^s(s)$.

principal_le_nhdsSet theorem

: 𝓟 s ≤ 𝓝ˢ s

Full source

theorem principal_le_nhdsSet : 𝓟 s ≤ 𝓝ˢ s := fun _s hs =>
  (subset_interior_iff_mem_nhdsSet.mpr hs).trans interior_subset

Principal Filter is Contained in Neighborhood Filter

Informal description

For any set $s$ in a topological space, the principal filter $\mathcal{P}(s)$ is contained in the neighborhood filter $\mathcal{N}^s(s)$ of $s$. In other words, every superset of $s$ in the principal filter is also a neighborhood of $s$.

subset_of_mem_nhdsSet theorem

(h : t ∈ 𝓝ˢ s) : s ⊆ t

Full source

theorem subset_of_mem_nhdsSet (h : t ∈ 𝓝ˢ s) : s ⊆ t := principal_le_nhdsSet h

Neighborhood Filter Contains Subset Relation: $t \in \mathcal{N}^s(s) \implies s \subseteq t$

Informal description

For any sets $s$ and $t$ in a topological space, if $t$ belongs to the neighborhood filter $\mathcal{N}^s(s)$ of $s$, then $s$ is a subset of $t$, i.e., $s \subseteq t$.

Filter.Eventually.self_of_nhdsSet theorem

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

Full source

theorem Filter.Eventually.self_of_nhdsSet {p : X → Prop} (h : ∀ᶠ x in 𝓝ˢ s, p x) : ∀ x ∈ s, p x :=
  principal_le_nhdsSet h

Neighborhood Eventual Property Implies Pointwise Property on Set

Informal description

For any predicate $p$ on a topological space $X$, if $p(x)$ holds for all $x$ in a neighborhood of a set $s$, then $p(x)$ holds for all $x \in s$.

Filter.EventuallyEq.self_of_nhdsSet theorem

{Y} {f g : X → Y} (h : f =ᶠ[𝓝ˢ s] g) : EqOn f g s

Full source

nonrec theorem Filter.EventuallyEq.self_of_nhdsSet {Y} {f g : X → Y} (h : f =ᶠ[𝓝ˢ s] g) :
    EqOn f g s :=
  h.self_of_nhdsSet

Eventual Equality in Neighborhood Filter Implies Pointwise Equality on Set

Informal description

For any topological space $X$, any type $Y$, and any functions $f, g : X \to Y$, if $f$ and $g$ are eventually equal in the neighborhood filter $\mathcal{N}^s(s)$ of a set $s \subseteq X$, then $f$ and $g$ are equal on $s$, i.e., $f(x) = g(x)$ for all $x \in s$.

nhdsSet_eq_principal_iff theorem

: 𝓝ˢ s = 𝓟 s ↔ IsOpen s

Full source

@[simp]
theorem nhdsSet_eq_principal_iff : 𝓝ˢ𝓝ˢ s = 𝓟 s ↔ IsOpen s := by
  rw [← principal_le_nhdsSet.le_iff_eq, le_principal_iff, mem_nhdsSet_iff_forall,
    isOpen_iff_mem_nhds]

Neighborhood Filter Equals Principal Filter if and only if Set is Open

Informal description

The neighborhood filter $\mathcal{N}(s)$ of a set $s$ is equal to the principal filter $\mathcal{P}(s)$ if and only if $s$ is an open set.

nhdsSet_interior theorem

: 𝓝ˢ (interior s) = 𝓟 (interior s)

Full source

@[simp]
theorem nhdsSet_interior : 𝓝ˢ (interior s) = 𝓟 (interior s) :=
  isOpen_interior.nhdsSet_eq

Neighborhood Filter of Interior Equals Principal Filter

Informal description

The neighborhood filter of the interior of a set $s$ in a topological space is equal to the principal filter generated by the interior of $s$, i.e., $\mathcal{N}^s(\text{interior}(s)) = \mathcal{P}(\text{interior}(s))$.

nhdsSet_singleton theorem

: 𝓝ˢ { x } = 𝓝 x

Full source

@[simp]
theorem nhdsSet_singleton : 𝓝ˢ {x} = 𝓝 x := by simp [nhdsSet]

Neighborhood Filter of Singleton Equals Point Neighborhood Filter

Informal description

The neighborhood filter of a singleton set $\{x\}$ in a topological space is equal to the neighborhood filter of the point $x$, i.e., $\mathcal{N}(\{x\}) = \mathcal{N}(x)$.

mem_nhdsSet_interior theorem

: s ∈ 𝓝ˢ (interior s)

Full source

theorem mem_nhdsSet_interior : s ∈ 𝓝ˢ (interior s) :=
  subset_interior_iff_mem_nhdsSet.mp Subset.rfl

Set Belongs to Neighborhood Filter of Its Interior

Informal description

For any set $s$ in a topological space, the set $s$ belongs to the neighborhood filter of its interior, i.e., $s \in \mathcal{N}^s(\text{interior}(s))$.

nhdsSet_empty theorem

: 𝓝ˢ (∅ : Set X) = ⊥

Full source

@[simp]
theorem nhdsSet_empty : 𝓝ˢ (∅ : Set X) = ⊥ := by rw [isOpen_empty.nhdsSet_eq, principal_empty]

Neighborhood Filter of Empty Set is Bottom Filter

Informal description

The neighborhood filter of the empty set in a topological space $X$ is equal to the bottom filter $\bot$, i.e., $\mathcal{N}^s(\emptyset) = \bot$.

mem_nhdsSet_empty theorem

: s ∈ 𝓝ˢ (∅ : Set X)

Full source

theorem mem_nhdsSet_empty : s ∈ 𝓝ˢ (∅ : Set X) := by simp

Every Set Belongs to Neighborhood Filter of Empty Set

Informal description

For any set $s$ in a topological space $X$, the set $s$ belongs to the neighborhood filter of the empty set, i.e., $s \in \mathcal{N}^s(\emptyset)$.

nhdsSet_univ theorem

: 𝓝ˢ (univ : Set X) = ⊤

Full source

@[simp]
theorem nhdsSet_univ : 𝓝ˢ (univ : Set X) = ⊤ := by rw [isOpen_univ.nhdsSet_eq, principal_univ]

Neighborhood Filter of the Entire Space is Trivial

Informal description

The neighborhood filter of the entire set $X$ in a topological space is equal to the trivial filter $\top$, i.e., $\mathcal{N}^s(X) = \top$.

nhdsSet_mono theorem

(h : s ⊆ t) : 𝓝ˢ s ≤ 𝓝ˢ t

Full source

@[gcongr, mono]
theorem nhdsSet_mono (h : s ⊆ t) : 𝓝ˢ s ≤ 𝓝ˢ t :=
  sSup_le_sSup <| image_subset _ h

Monotonicity of Neighborhood Filters with Respect to Subset Inclusion

Informal description

For any subsets $s$ and $t$ of a topological space $X$, if $s \subseteq t$, then the neighborhood filter of $s$ is finer than the neighborhood filter of $t$, i.e., $\mathcal{N}_s \leq \mathcal{N}_t$.

monotone_nhdsSet theorem

: Monotone (𝓝ˢ : Set X → Filter X)

Full source

theorem monotone_nhdsSet : Monotone (𝓝ˢ : Set X → Filter X) := fun _ _ => nhdsSet_mono

Monotonicity of the Neighborhood Filter Function

Informal description

The neighborhood filter function $\mathcal{N}^s : \text{Set } X \to \text{Filter } X$ is monotone, meaning that for any subsets $s$ and $t$ of a topological space $X$, if $s \subseteq t$, then $\mathcal{N}^s(s) \leq \mathcal{N}^s(t)$.

nhds_le_nhdsSet theorem

(h : x ∈ s) : 𝓝 x ≤ 𝓝ˢ s

Full source

theorem nhds_le_nhdsSet (h : x ∈ s) : 𝓝 x ≤ 𝓝ˢ s :=
  le_sSup <| mem_image_of_mem _ h

Neighborhood Filter of a Point in a Set is Finer than the Neighborhood Filter of the Set

Informal description

For any point $x$ in a set $s$ in a topological space, the neighborhood filter $\mathcal{N}(x)$ of $x$ is finer than the neighborhood filter $\mathcal{N}^s(s)$ of the set $s$, i.e., $\mathcal{N}(x) \leq \mathcal{N}^s(s)$.

nhdsSet_union theorem

(s t : Set X) : 𝓝ˢ (s ∪ t) = 𝓝ˢ s ⊔ 𝓝ˢ t

Full source

@[simp]
theorem nhdsSet_union (s t : Set X) : 𝓝ˢ (s ∪ t) = 𝓝ˢ𝓝ˢ s ⊔ 𝓝ˢ t := by
  simp only [nhdsSet, image_union, sSup_union]

Neighborhood Filter of Union is Supremum of Individual Filters

Informal description

For any two sets $s$ and $t$ in a topological space $X$, the neighborhood filter of their union $\mathcal{N}(s \cup t)$ is equal to the supremum of their individual neighborhood filters $\mathcal{N}(s) \sqcup \mathcal{N}(t)$.

union_mem_nhdsSet theorem

(h₁ : s₁ ∈ 𝓝ˢ t₁) (h₂ : s₂ ∈ 𝓝ˢ t₂) : s₁ ∪ s₂ ∈ 𝓝ˢ (t₁ ∪ t₂)

Full source

theorem union_mem_nhdsSet (h₁ : s₁ ∈ 𝓝ˢ t₁) (h₂ : s₂ ∈ 𝓝ˢ t₂) : s₁ ∪ s₂s₁ ∪ s₂ ∈ 𝓝ˢ (t₁ ∪ t₂) := by
  rw [nhdsSet_union]
  exact union_mem_sup h₁ h₂

Union of Neighborhoods is Neighborhood of Union

Informal description

For any two sets $s_1, s_2$ and $t_1, t_2$ in a topological space $X$, if $s_1$ is a neighborhood of $t_1$ and $s_2$ is a neighborhood of $t_2$, then the union $s_1 \cup s_2$ is a neighborhood of the union $t_1 \cup t_2$.

nhdsSet_insert theorem

(x : X) (s : Set X) : 𝓝ˢ (insert x s) = 𝓝 x ⊔ 𝓝ˢ s

Full source

@[simp]
theorem nhdsSet_insert (x : X) (s : Set X) : 𝓝ˢ (insert x s) = 𝓝𝓝 x ⊔ 𝓝ˢ s := by
  rw [insert_eq, nhdsSet_union, nhdsSet_singleton]

Neighborhood Filter of Inserted Point Equals Supremum of Point and Set Filters

Informal description

For any point $x$ and any set $s$ in a topological space $X$, the neighborhood filter of the set $\{x\} \cup s$ is equal to the supremum of the neighborhood filter of $x$ and the neighborhood filter of $s$, i.e., $\mathcal{N}(\{x\} \cup s) = \mathcal{N}(x) \sqcup \mathcal{N}(s)$.

nhdsSet_inter_le theorem

(s t : Set X) : 𝓝ˢ (s ∩ t) ≤ 𝓝ˢ s ⊓ 𝓝ˢ t

Full source

theorem nhdsSet_inter_le (s t : Set X) : 𝓝ˢ (s ∩ t) ≤ 𝓝ˢ𝓝ˢ s ⊓ 𝓝ˢ t :=
  (monotone_nhdsSet (X := X)).map_inf_le s t

Neighborhood Filter of Intersection is Bounded by Infimum of Filters

Informal description

For any two subsets $s$ and $t$ of a topological space $X$, the neighborhood filter of their intersection $\mathcal{N}^s(s \cap t)$ is contained in the infimum of the neighborhood filters of $s$ and $t$, i.e., \[ \mathcal{N}^s(s \cap t) \leq \mathcal{N}^s(s) \sqcap \mathcal{N}^s(t). \]

nhdsSet_iInter_le theorem

{ι : Sort*} (s : ι → Set X) : 𝓝ˢ (⋂ i, s i) ≤ ⨅ i, 𝓝ˢ (s i)

Full source

theorem nhdsSet_iInter_le {ι : Sort*} (s : ι → Set X) : 𝓝ˢ (⋂ i, s i) ≤ ⨅ i, 𝓝ˢ (s i) :=
  (monotone_nhdsSet (X := X)).map_iInf_le

Neighborhood Filter of Intersection is Bounded by Infimum of Filters

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ in a topological space $X$, the neighborhood filter of the intersection $\bigcap_i s_i$ is contained in the infimum of the neighborhood filters of each set $s_i$, i.e., \[ \mathcal{N}^s\left(\bigcap_i s_i\right) \leq \bigwedge_i \mathcal{N}^s(s_i). \]

nhdsSet_sInter_le theorem

(s : Set (Set X)) : 𝓝ˢ (⋂₀ s) ≤ ⨅ x ∈ s, 𝓝ˢ x

Full source

theorem nhdsSet_sInter_le (s : Set (Set X)) : 𝓝ˢ (⋂₀ s) ≤ ⨅ x ∈ s, 𝓝ˢ x :=
  (monotone_nhdsSet (X := X)).map_sInf_le

Neighborhood Filter of Intersection is Contained in Infimum of Neighborhood Filters

Informal description

For any family of sets $s$ in a topological space $X$, the neighborhood filter of the intersection $\bigcap₀ s$ is contained in the infimum of the neighborhood filters of each set in $s$, i.e., \[ \mathcal{N}^s\left(\bigcap₀ s\right) \leq \biginf_{x \in s} \mathcal{N}^s(x). \]

IsClosed.nhdsSet_le_sup theorem

(h : IsClosed t) : 𝓝ˢ s ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓟 (tᶜ)

Full source

theorem IsClosed.nhdsSet_le_sup (h : IsClosed t) : 𝓝ˢ s ≤ 𝓝ˢ𝓝ˢ (s ∩ t) ⊔ 𝓟 (tᶜ) :=
  calc
    𝓝ˢ s = 𝓝ˢ (s ∩ ts ∩ t ∪ s ∩ tᶜ) := by rw [Set.inter_union_compl s t]
    _ = 𝓝ˢ𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ (s ∩ tᶜ) := by rw [nhdsSet_union]
    _ ≤ 𝓝ˢ𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ (tᶜ) := sup_le_sup_left (monotone_nhdsSet inter_subset_right) _
    _ = 𝓝ˢ𝓝ˢ (s ∩ t) ⊔ 𝓟 (tᶜ) := by rw [h.isOpen_compl.nhdsSet_eq]

Neighborhood Filter of a Set is Bounded by Intersection with Closed Set and Complement

Informal description

For any closed subset $t$ of a topological space $X$, the neighborhood filter $\mathcal{N}^s(s)$ of a subset $s$ is contained in the supremum of the neighborhood filter $\mathcal{N}^s(s \cap t)$ and the principal filter generated by the complement $t^c$ of $t$, i.e., \[ \mathcal{N}^s(s) \leq \mathcal{N}^s(s \cap t) \sqcup \mathcal{P}(t^c). \]

IsClosed.nhdsSet_le_sup' theorem

(h : IsClosed t) : 𝓝ˢ s ≤ 𝓝ˢ (t ∩ s) ⊔ 𝓟 (tᶜ)

Full source

theorem IsClosed.nhdsSet_le_sup' (h : IsClosed t) :
    𝓝ˢ s ≤ 𝓝ˢ𝓝ˢ (t ∩ s) ⊔ 𝓟 (tᶜ) := by rw [Set.inter_comm]; exact h.nhdsSet_le_sup s

Neighborhood Filter Bound for Intersection with Closed Set

Informal description

For any closed subset $t$ of a topological space $X$, the neighborhood filter $\mathcal{N}(s)$ of a subset $s$ is bounded above by the supremum of the neighborhood filter $\mathcal{N}(t \cap s)$ and the principal filter generated by the complement $t^c$, i.e., \[ \mathcal{N}(s) \leq \mathcal{N}(t \cap s) \sqcup \mathcal{P}(t^c). \]

Filter.Eventually.eventually_nhdsSet theorem

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

Full source

theorem Filter.Eventually.eventually_nhdsSet {p : X → Prop} (h : ∀ᶠ y in 𝓝ˢ s, p y) :
    ∀ᶠ y in 𝓝ˢ s, ∀ᶠ x in 𝓝 y, p x :=
  eventually_nhdsSet_iff_forall.mpr fun x x_in ↦
    (eventually_nhdsSet_iff_forall.mp h x x_in).eventually_nhds

Eventual Truth in Neighborhood Filter Implies Pointwise Eventual Truth in Neighborhoods

Informal description

For any predicate $p$ on a topological space $X$ and any subset $s \subseteq X$, if $p$ holds eventually in the neighborhood filter $\mathcal{N}(s)$ of $s$, then for eventually all $y$ in $\mathcal{N}(s)$, the predicate $p$ holds eventually in the neighborhood filter $\mathcal{N}(y)$ of $y$.

Filter.Eventually.union_nhdsSet theorem

{p : X → Prop} : (∀ᶠ x in 𝓝ˢ (s ∪ t), p x) ↔ (∀ᶠ x in 𝓝ˢ s, p x) ∧ ∀ᶠ x in 𝓝ˢ t, p x

Full source

theorem Filter.Eventually.union_nhdsSet {p : X → Prop} :
    (∀ᶠ x in 𝓝ˢ (s ∪ t), p x) ↔ (∀ᶠ x in 𝓝ˢ s, p x) ∧ ∀ᶠ x in 𝓝ˢ t, p x := by
  rw [nhdsSet_union, eventually_sup]

Eventual Property in Union Neighborhood Filter iff in Both Individual Filters

Informal description

For any predicate $p$ on a topological space $X$ and any sets $s, t \subseteq X$, the predicate $p$ holds eventually in the neighborhood filter of $s \cup t$ if and only if it holds eventually in both the neighborhood filter of $s$ and the neighborhood filter of $t$. In other words: \[ (\forall^\infty x \in \mathcal{N}(s \cup t),\, p(x)) \leftrightarrow (\forall^\infty x \in \mathcal{N}(s),\, p(x)) \land (\forall^\infty x \in \mathcal{N}(t),\, p(x)) \]

Filter.Eventually.union theorem

{p : X → Prop} (hs : ∀ᶠ x in 𝓝ˢ s, p x) (ht : ∀ᶠ x in 𝓝ˢ t, p x) : ∀ᶠ x in 𝓝ˢ (s ∪ t), p x

Full source

theorem Filter.Eventually.union {p : X → Prop} (hs : ∀ᶠ x in 𝓝ˢ s, p x) (ht : ∀ᶠ x in 𝓝ˢ t, p x) :
    ∀ᶠ x in 𝓝ˢ (s ∪ t), p x :=
  Filter.Eventually.union_nhdsSet.mpr ⟨hs, ht⟩

Eventual Property in Union Neighborhood Filter from Individual Filters

Informal description

For any predicate $p$ on a topological space $X$ and any subsets $s, t \subseteq X$, if $p$ holds eventually in the neighborhood filter $\mathcal{N}(s)$ of $s$ and also in the neighborhood filter $\mathcal{N}(t)$ of $t$, then $p$ holds eventually in the neighborhood filter $\mathcal{N}(s \cup t)$ of the union $s \cup t$.

nhdsSet_iUnion theorem

{ι : Sort*} (s : ι → Set X) : 𝓝ˢ (⋃ i, s i) = ⨆ i, 𝓝ˢ (s i)

Full source

theorem nhdsSet_iUnion {ι : Sort*} (s : ι → Set X) : 𝓝ˢ (⋃ i, s i) = ⨆ i, 𝓝ˢ (s i) := by
  simp only [nhdsSet, image_iUnion, sSup_iUnion (β := Filter X)]

Neighborhood Filter of Union Equals Supremum of Neighborhood Filters

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ in a topological space $X$, the neighborhood filter of the union $\bigcup_i s_i$ is equal to the supremum of the neighborhood filters of each individual set $s_i$. In symbols: \[ \mathcal{N}\left(\bigcup_i s_i\right) = \bigsqcup_i \mathcal{N}(s_i) \]

eventually_nhdsSet_iUnion₂ theorem

 {ι : Sort*} {p : ι → Prop} {s : ι → Set X} {P : X → Prop} :
  (∀ᶠ x in 𝓝ˢ (⋃ (i) (_ : p i), s i), P x) ↔ ∀ i, p i → ∀ᶠ x in 𝓝ˢ (s i), P x

Full source

theorem eventually_nhdsSet_iUnion₂ {ι : Sort*} {p : ι → Prop} {s : ι → Set X} {P : X → Prop} :
    (∀ᶠ x in 𝓝ˢ (⋃ (i) (_ : p i), s i), P x) ↔ ∀ i, p i → ∀ᶠ x in 𝓝ˢ (s i), P x := by
  simp only [nhdsSet_iUnion, eventually_iSup]

Neighborhood Eventual Property of Filtered Union Equals Pointwise Neighborhood Eventual Properties

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ in a topological space $X$, any predicate $p$ on $\iota$, and any predicate $P$ on $X$, the following are equivalent: 1. $P(x)$ holds for all $x$ in some neighborhood of $\bigcup_{i \text{ with } p(i)} s_i$. 2. For each index $i$, if $p(i)$ holds, then $P(x)$ holds for all $x$ in some neighborhood of $s_i$. In symbols: \[ \left(\forall^\mathcal{N} x \in \bigcup_{\substack{i \\ p(i)}} s_i, P(x)\right) \leftrightarrow \left(\forall i, p(i) \to \forall^\mathcal{N} x \in s_i, P(x)\right) \] where $\forall^\mathcal{N}$ denotes "for all $x$ in some neighborhood".

eventually_nhdsSet_iUnion theorem

 {ι : Sort*} {s : ι → Set X} {P : X → Prop} : (∀ᶠ x in 𝓝ˢ (⋃ i, s i), P x) ↔ ∀ i, ∀ᶠ x in 𝓝ˢ (s i), P x

Full source

theorem eventually_nhdsSet_iUnion {ι : Sort*} {s : ι → Set X} {P : X → Prop} :
    (∀ᶠ x in 𝓝ˢ (⋃ i, s i), P x) ↔ ∀ i, ∀ᶠ x in 𝓝ˢ (s i), P x := by
  simp only [nhdsSet_iUnion, eventually_iSup]

Neighborhood Eventual Property of Union Equals Pointwise Neighborhood Eventual Properties

Informal description

For any indexed family of sets $\{s_i\}_{i \in \iota}$ in a topological space $X$ and any predicate $P$ on $X$, the following are equivalent: 1. $P(x)$ holds for all $x$ in some neighborhood of $\bigcup_i s_i$. 2. For each index $i$, $P(x)$ holds for all $x$ in some neighborhood of $s_i$. In symbols: \[ \left(\forall^\mathcal{N} x \in \bigcup_i s_i, P(x)\right) \leftrightarrow \left(\forall i, \forall^\mathcal{N} x \in s_i, P(x)\right) \] where $\forall^\mathcal{N}$ denotes "for all $x$ in some neighborhood".

Main Properties