# Neighborhoods relative to a subset #

This file develops API on the relative version `nhdsWithin` of `nhds`, which is defined in previous definition files.

Their basic properties studied in this file include the relationship between neighborhood filters relative to a set and neighborhood filters in the corresponding subtype, and are in later files used to develop relativ versions `ContinuousOn` and `ContinuousWithinAt` of `Continuous` and `ContinuousAt`.

## Notation #

- `𝓝 x`: the filter of neighborhoods of a point `x`;
- `𝓟 s`: the principal filter of a set `s`;
- `𝓝[s] x`: the filter `nhdsWithin x s` of neighborhoods of a point `x` within a set `s`.

## Properties of the neighborhood-within filter #

source
@[simp]
theorem nhds_bind_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} :
((nhds a).bind fun (x : α) => nhdsWithin x s) = nhdsWithin a s
source
@[simp]
theorem eventually_nhds_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop} :
(∀ᶠ (y : α) in nhds a, ∀ᶠ (x : α) in nhdsWithin y s, p x) ↔ ∀ᶠ (x : α) in nhdsWithin a s, p x
source
theorem eventually_nhdsWithin_iff {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop} :
(∀ᶠ (x : α) in nhdsWithin a s, p x) ↔ ∀ᶠ (x : α) in nhds a, x ∈ s → p x
source
theorem frequently_nhdsWithin_iff {α : Type u_1} [TopologicalSpace α] {z : α} {s : Set α} {p : α → Prop} :
(∃ᶠ (x : α) in nhdsWithin z s, p x) ↔ ∃ᶠ (x : α) in nhds z, p x ∧ x ∈ s
source
theorem mem_closure_ne_iff_frequently_within {α : Type u_1} [TopologicalSpace α] {z : α} {s : Set α} :
z ∈ closure (s \ {z}) ↔ ∃ᶠ (x : α) in nhdsWithin z {z}ᶜ, x ∈ s
source
@[simp]
theorem eventually_eventually_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop} :
(∀ᶠ (y : α) in nhdsWithin a s, ∀ᶠ (x : α) in nhdsWithin y s, p x) ↔ ∀ᶠ (x : α) in nhdsWithin a s, p x
source
@[simp]
theorem eventually_mem_nhdsWithin_iff {α : Type u_1} [TopologicalSpace α] {x : α} {s t : Set α} :
(∀ᶠ (x' : α) in nhdsWithin x s, t ∈ nhdsWithin x' s) ↔ t ∈ nhdsWithin x s
source
theorem nhdsWithin_eq {α : Type u_1} [TopologicalSpace α] (a : α) (s : Set α) :
nhdsWithin a s = ⨅ t ∈ {t : Set α | a ∈ t ∧ IsOpen t}, Filter.principal (t ∩ s)
source
@[simp]
theorem nhdsWithin_univ {α : Type u_1} [TopologicalSpace α] (a : α) :
nhdsWithin a Set.univ = nhds a
source
theorem nhdsWithin_hasBasis {α : Type u_1} [TopologicalSpace α] {ι : Sort u_5} {p : ι → Prop} {s : ι → Set α} {a : α} (h : (nhds a).HasBasis p s) (t : Set α) :
(nhdsWithin a t).HasBasis p fun (i : ι) => s i ∩ t
source
theorem nhdsWithin_basis_open {α : Type u_1} [TopologicalSpace α] (a : α) (t : Set α) :
(nhdsWithin a t).HasBasis (fun (u : Set α) => a ∈ u ∧ IsOpen u) fun (u : Set α) => u ∩ t
source
theorem mem_nhdsWithin {α : Type u_1} [TopologicalSpace α] {t : Set α} {a : α} {s : Set α} :
t ∈ nhdsWithin a s ↔ ∃ (u : Set α), IsOpen u ∧ a ∈ u ∧ u ∩ s ⊆ t
source
theorem mem_nhdsWithin_iff_exists_mem_nhds_inter {α : Type u_1} [TopologicalSpace α] {t : Set α} {a : α} {s : Set α} :
t ∈ nhdsWithin a s ↔ ∃ u ∈ nhds a, u ∩ s ⊆ t
source
theorem diff_mem_nhdsWithin_compl {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} (hs : s ∈ nhds x) (t : Set α) :
s \ t ∈ nhdsWithin x t ᶜ
source
theorem diff_mem_nhdsWithin_diff {α : Type u_1} [TopologicalSpace α] {x : α} {s t : Set α} (hs : s ∈ nhdsWithin x t) (t' : Set α) :
s \ t' ∈ nhdsWithin x (t \ t')
source
theorem nhds_of_nhdsWithin_of_nhds {α : Type u_1} [TopologicalSpace α] {s t : Set α} {a : α} (h1 : s ∈ nhds a) (h2 : t ∈ nhdsWithin a s) :
t ∈ nhds a
source
theorem mem_nhdsWithin_iff_eventually {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} :
t ∈ nhdsWithin x s ↔ ∀ᶠ (y : α) in nhds x, y ∈ s → y ∈ t
source
theorem mem_nhdsWithin_iff_eventuallyEq {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} :
t ∈ nhdsWithin x s ↔ s =ᶠ[nhds x] s ∩ t
source
theorem mem_nhdsWithin_inter_self {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} :
t ∈ nhdsWithin x (s ∩ t)
source
theorem mem_nhdsWithin_self_inter {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} :
s ∈ nhdsWithin x (s ∩ t)
source
theorem nhdsWithin_eq_iff_eventuallyEq {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} :
nhdsWithin x s = nhdsWithin x t ↔ s =ᶠ[nhds x] t
source
theorem nhdsWithin_le_iff {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} :
nhdsWithin x s ≤ nhdsWithin x t ↔ t ∈ nhdsWithin x s
source
theorem preimage_nhdsWithin_coinduced' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {X : α → β} {s : Set β} {t : Set α} {a : α} (h : a ∈ t) (hs : s ∈ nhds (X a)) :
X ⁻¹' s ∈ nhdsWithin a t
source
theorem mem_nhdsWithin_of_mem_nhds {α : Type u_1} [TopologicalSpace α] {s t : Set α} {a : α} (h : s ∈ nhds a) :
s ∈ nhdsWithin a t
source
theorem self_mem_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} :
s ∈ nhdsWithin a s
source
theorem eventually_mem_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} :
∀ᶠ (x : α) in nhdsWithin a s, x ∈ s
source
theorem inter_mem_nhdsWithin {α : Type u_1} [TopologicalSpace α] (s : Set α) {t : Set α} {a : α} (h : t ∈ nhds a) :
s ∩ t ∈ nhdsWithin a s
source
theorem pure_le_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} (ha : a ∈ s) :
pure a ≤ nhdsWithin a s
source
theorem mem_of_mem_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s t : Set α} (ha : a ∈ s) (ht : t ∈ nhdsWithin a s) :
a ∈ t
source
theorem Filter.Eventually.self_of_nhdsWithin {α : Type u_1} [TopologicalSpace α] {p : α → Prop} {s : Set α} {x : α} (h : ∀ᶠ (y : α) in nhdsWithin x s, p y) (hx : x ∈ s) :
p x
source
theorem tendsto_const_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {l : Filter β} {s : Set α} {a : α} (ha : a ∈ s) :
Filter.Tendsto (fun (x : β) => a) l (nhdsWithin a s)
source
theorem nhdsWithin_restrict'' {α : Type u_1} [TopologicalSpace α] {a : α} (s : Set α) {t : Set α} (h : t ∈ nhdsWithin a s) :
nhdsWithin a s = nhdsWithin a (s ∩ t)
source
theorem nhdsWithin_restrict' {α : Type u_1} [TopologicalSpace α] {a : α} (s : Set α) {t : Set α} (h : t ∈ nhds a) :
nhdsWithin a s = nhdsWithin a (s ∩ t)
source
theorem nhdsWithin_restrict {α : Type u_1} [TopologicalSpace α] {a : α} (s : Set α) {t : Set α} (h₀ : a ∈ t) (h₁ : IsOpen t) :
nhdsWithin a s = nhdsWithin a (s ∩ t)
source
theorem nhdsWithin_le_of_mem {α : Type u_1} [TopologicalSpace α] {a : α} {s t : Set α} (h : s ∈ nhdsWithin a t) :
nhdsWithin a t ≤ nhdsWithin a s
source
theorem nhdsWithin_le_nhds {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} :
nhdsWithin a s ≤ nhds a
source
theorem nhdsWithin_eq_nhdsWithin' {α : Type u_1} [TopologicalSpace α] {a : α} {s t u : Set α} (hs : s ∈ nhds a) (h₂ : t ∩ s = u ∩ s) :
nhdsWithin a t = nhdsWithin a u
source
theorem nhdsWithin_eq_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s t u : Set α} (h₀ : a ∈ s) (h₁ : IsOpen s) (h₂ : t ∩ s = u ∩ s) :
nhdsWithin a t = nhdsWithin a u
source
@[simp]
theorem nhdsWithin_eq_nhds {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} :
nhdsWithin a s = nhds a ↔ s ∈ nhds a
source
theorem IsOpen.nhdsWithin_eq {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} (h : IsOpen s) (ha : a ∈ s) :
nhdsWithin a s = nhds a
source
theorem preimage_nhds_within_coinduced {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {X : α → β} {s : Set β} {t : Set α} {a : α} (h : a ∈ t) (ht : IsOpen t) (hs : s ∈ nhds (X a)) :
X ⁻¹' s ∈ nhds a
source
@[simp]
theorem nhdsWithin_empty {α : Type u_1} [TopologicalSpace α] (a : α) :
nhdsWithin a ∅ = ⊥
source
theorem nhdsWithin_union {α : Type u_1} [TopologicalSpace α] (a : α) (s t : Set α) :
nhdsWithin a (s ∪ t) = nhdsWithin a s ⊔ nhdsWithin a t
source
theorem nhds_eq_nhdsWithin_sup_nhdsWithin {α : Type u_1} [TopologicalSpace α] (b : α) {I₁ I₂ : Set α} (hI : Set.univ = I₁ ∪ I₂) :
nhds b = nhdsWithin b I₁ ⊔ nhdsWithin b I₂
source
theorem union_mem_nhds_of_mem_nhdsWithin {α : Type u_1} [TopologicalSpace α] {b : α} {I₁ I₂ : Set α} (h : Set.univ = I₁ ∪ I₂) {L : Set α} (hL : L ∈ nhdsWithin b I₁) {R : Set α} (hR : R ∈ nhdsWithin b I₂) :
L ∪ R ∈ nhds b

If `L` and `R` are neighborhoods of `b` within sets whose union is `Set.univ`, then `L ∪ R` is a neighborhood of `b`.

source
theorem punctured_nhds_eq_nhdsWithin_sup_nhdsWithin {α : Type u_1} [TopologicalSpace α] [LinearOrder α] {x : α} :
nhdsWithin x {x}ᶜ = nhdsWithin x (Set.Iio x) ⊔ nhdsWithin x (Set.Ioi x)

Writing a punctured neighborhood filter as a sup of left and right filters.

source
theorem nhds_of_Ici_Iic {α : Type u_1} [TopologicalSpace α] [LinearOrder α] {b : α} {L : Set α} (hL : L ∈ nhdsWithin b (Set.Iic b)) {R : Set α} (hR : R ∈ nhdsWithin b (Set.Ici b)) :
L ∩ Set.Iic b ∪ R ∩ Set.Ici b ∈ nhds b

Obtain a "predictably-sided" neighborhood of `b` from two one-sided neighborhoods.

source
theorem nhdsWithin_biUnion {α : Type u_1} [TopologicalSpace α] {ι : Type u_5} {I : Set ι} (hI : I.Finite) (s : ι → Set α) (a : α) :
nhdsWithin a (⋃ i ∈ I, s i) = ⨆ i ∈ I, nhdsWithin a (s i)
source
theorem nhdsWithin_sUnion {α : Type u_1} [TopologicalSpace α] {S : Set (Set α)} (hS : S.Finite) (a : α) :
nhdsWithin a (⋃₀ S) = ⨆ s ∈ S, nhdsWithin a s
source
theorem nhdsWithin_iUnion {α : Type u_1} [TopologicalSpace α] {ι : Sort u_5} [Finite ι] (s : ι → Set α) (a : α) :
nhdsWithin a (⋃ (i : ι), s i) = ⨆ (i : ι), nhdsWithin a (s i)
source
theorem nhdsWithin_inter {α : Type u_1} [TopologicalSpace α] (a : α) (s t : Set α) :
nhdsWithin a (s ∩ t) = nhdsWithin a s ⊓ nhdsWithin a t
source
theorem nhdsWithin_inter' {α : Type u_1} [TopologicalSpace α] (a : α) (s t : Set α) :
nhdsWithin a (s ∩ t) = nhdsWithin a s ⊓ Filter.principal t
source
theorem nhdsWithin_inter_of_mem {α : Type u_1} [TopologicalSpace α] {a : α} {s t : Set α} (h : s ∈ nhdsWithin a t) :
nhdsWithin a (s ∩ t) = nhdsWithin a t
source
theorem nhdsWithin_inter_of_mem' {α : Type u_1} [TopologicalSpace α] {a : α} {s t : Set α} (h : t ∈ nhdsWithin a s) :
nhdsWithin a (s ∩ t) = nhdsWithin a s
source
@[simp]
theorem nhdsWithin_singleton {α : Type u_1} [TopologicalSpace α] (a : α) :
nhdsWithin a {a} = pure a
source
@[simp]
theorem nhdsWithin_insert {α : Type u_1} [TopologicalSpace α] (a : α) (s : Set α) :
nhdsWithin a (insert a s) = pure a ⊔ nhdsWithin a s
source
theorem mem_nhdsWithin_insert {α : Type u_1} [TopologicalSpace α] {a : α} {s t : Set α} :
t ∈ nhdsWithin a (insert a s) ↔ a ∈ t ∧ t ∈ nhdsWithin a s
source
theorem insert_mem_nhdsWithin_insert {α : Type u_1} [TopologicalSpace α] {a : α} {s t : Set α} (h : t ∈ nhdsWithin a s) :
insert a t ∈ nhdsWithin a (insert a s)
source
theorem insert_mem_nhds_iff {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} :
insert a s ∈ nhds a ↔ s ∈ nhdsWithin a {a}ᶜ
source
@[simp]
theorem nhdsNE_sup_pure {α : Type u_1} [TopologicalSpace α] (a : α) :
nhdsWithin a {a}ᶜ ⊔ pure a = nhds a
source
@[simp]
theorem pure_sup_nhdsNE {α : Type u_1} [TopologicalSpace α] (a : α) :
pure a ⊔ nhdsWithin a {a}ᶜ = nhds a
source
theorem continuousAt_iff_punctured_nhds {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {a : α} :
ContinuousAt f a ↔ Filter.Tendsto f (nhdsWithin a {a}ᶜ) (nhds (f a))
source
theorem nhdsWithin_prod {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s u : Set α} {t v : Set β} {a : α} {b : β} (hu : u ∈ nhdsWithin a s) (hv : v ∈ nhdsWithin b t) :
u ×ˢ v ∈ nhdsWithin (a, b) (s ×ˢ t)
source
theorem Filter.EventuallyEq.mem_interior {α : Type u_1} [TopologicalSpace α] {x : α} {s t : Set α} (hst : s =ᶠ[nhds x] t) (h : x ∈ interior s) :
x ∈ interior t
source
theorem Filter.EventuallyEq.mem_interior_iff {α : Type u_1} [TopologicalSpace α] {x : α} {s t : Set α} (hst : s =ᶠ[nhds x] t) :
x ∈ interior s ↔ x ∈ interior t
source
theorem nhdsWithin_pi_eq' {ι : Type u_5} {X : ι → Type u_6} [(i : ι) → TopologicalSpace (X i)] {I : Set ι} (hI : I.Finite) (s : (i : ι) → Set (X i)) (x : (i : ι) → X i) :
nhdsWithin x (I.pi s) = ⨅ (i : ι), Filter.comap (fun (x : (i : ι) → X i) => x i) (nhds (x i) ⊓ ⨅ (_ : i ∈ I), Filter.principal (s i))
source
theorem nhdsWithin_pi_eq {ι : Type u_5} {X : ι → Type u_6} [(i : ι) → TopologicalSpace (X i)] {I : Set ι} (hI : I.Finite) (s : (i : ι) → Set (X i)) (x : (i : ι) → X i) :
nhdsWithin x (I.pi s) = (⨅ i ∈ I, Filter.comap (fun (x : (i : ι) → X i) => x i) (nhdsWithin (x i) (s i))) ⊓ ⨅ (i : ι), ⨅ (_ : i ∉ I), Filter.comap (fun (x : (i : ι) → X i) => x i) (nhds (x i))
source
theorem nhdsWithin_pi_univ_eq {ι : Type u_5} {X : ι → Type u_6} [(i : ι) → TopologicalSpace (X i)] [Finite ι] (s : (i : ι) → Set (X i)) (x : (i : ι) → X i) :
nhdsWithin x (Set.univ.pi s) = ⨅ (i : ι), Filter.comap (fun (x : (i : ι) → X i) => x i) (nhdsWithin (x i) (s i))
source
theorem nhdsWithin_pi_eq_bot {ι : Type u_5} {X : ι → Type u_6} [(i : ι) → TopologicalSpace (X i)] {I : Set ι} {s : (i : ι) → Set (X i)} {x : (i : ι) → X i} :
nhdsWithin x (I.pi s) = ⊥ ↔ ∃ i ∈ I, nhdsWithin (x i) (s i) = ⊥
source
theorem nhdsWithin_pi_neBot {ι : Type u_5} {X : ι → Type u_6} [(i : ι) → TopologicalSpace (X i)] {I : Set ι} {s : (i : ι) → Set (X i)} {x : (i : ι) → X i} :
(nhdsWithin x (I.pi s)).NeBot ↔ ∀ i ∈ I, (nhdsWithin (x i) (s i)).NeBot
source
instance instNeBotNhdsWithinUnivPi {ι : Type u_5} {X : ι → Type u_6} [(i : ι) → TopologicalSpace (X i)] {s : (i : ι) → Set (X i)} {x : (i : ι) → X i} [∀ (i : ι), (nhdsWithin (x i) (s i)).NeBot] :
(nhdsWithin x (Set.univ.pi s)).NeBot
source
instance Pi.instNeBotNhdsWithinIio {ι : Type u_5} {X : ι → Type u_6} [(i : ι) → TopologicalSpace (X i)] [Nonempty ι] [(i : ι) → Preorder (X i)] {x : (i : ι) → X i} [∀ (i : ι), (nhdsWithin (x i) (Set.Iio (x i))).NeBot] :
(nhdsWithin x (Set.Iio x)).NeBot
source
instance Pi.instNeBotNhdsWithinIoi {ι : Type u_5} {X : ι → Type u_6} [(i : ι) → TopologicalSpace (X i)] [Nonempty ι] [(i : ι) → Preorder (X i)] {x : (i : ι) → X i} [∀ (i : ι), (nhdsWithin (x i) (Set.Ioi (x i))).NeBot] :
(nhdsWithin x (Set.Ioi x)).NeBot
source
theorem Filter.Tendsto.piecewise_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f g : α → β} {t : Set α} [(x : α) → Decidable (x ∈ t)] {a : α} {s : Set α} {l : Filter β} (h₀ : Tendsto f (nhdsWithin a (s ∩ t)) l) (h₁ : Tendsto g (nhdsWithin a (s ∩ t ᶜ)) l) :
Tendsto (t.piecewise f g) (nhdsWithin a s) l
source
theorem Filter.Tendsto.if_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f g : α → β} {p : α → Prop} [DecidablePred p] {a : α} {s : Set α} {l : Filter β} (h₀ : Tendsto f (nhdsWithin a (s ∩ {x : α | p x})) l) (h₁ : Tendsto g (nhdsWithin a (s ∩ {x : α | ¬p x})) l) :
Tendsto (fun (x : α) => if p x then f x else g x) (nhdsWithin a s) l
source
theorem map_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] (f : α → β) (a : α) (s : Set α) :
Filter.map f (nhdsWithin a s) = ⨅ t ∈ {t : Set α | a ∈ t ∧ IsOpen t}, Filter.principal (f '' (t ∩ s))
source
theorem tendsto_nhdsWithin_mono_left {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → β} {a : α} {s t : Set α} {l : Filter β} (hst : s ⊆ t) (h : Filter.Tendsto f (nhdsWithin a t) l) :
Filter.Tendsto f (nhdsWithin a s) l
source
theorem tendsto_nhdsWithin_mono_right {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : β → α} {l : Filter β} {a : α} {s t : Set α} (hst : s ⊆ t) (h : Filter.Tendsto f l (nhdsWithin a s)) :
Filter.Tendsto f l (nhdsWithin a t)
source
theorem tendsto_nhdsWithin_of_tendsto_nhds {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → β} {a : α} {s : Set α} {l : Filter β} (h : Filter.Tendsto f (nhds a) l) :
Filter.Tendsto f (nhdsWithin a s) l
source
theorem eventually_mem_of_tendsto_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : β → α} {a : α} {s : Set α} {l : Filter β} (h : Filter.Tendsto f l (nhdsWithin a s)) :
∀ᶠ (i : β) in l, f i ∈ s
source
theorem tendsto_nhds_of_tendsto_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : β → α} {a : α} {s : Set α} {l : Filter β} (h : Filter.Tendsto f l (nhdsWithin a s)) :
Filter.Tendsto f l (nhds a)
source
theorem nhdsWithin_neBot_of_mem {α : Type u_1} [TopologicalSpace α] {s : Set α} {x : α} (hx : x ∈ s) :
(nhdsWithin x s).NeBot
source
theorem IsClosed.mem_of_nhdsWithin_neBot {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : IsClosed s) {x : α} (hx : (nhdsWithin x s).NeBot) :
x ∈ s
source
theorem DenseRange.nhdsWithin_neBot {α : Type u_1} [TopologicalSpace α] {ι : Type u_5} {f : ι → α} (h : DenseRange f) (x : α) :
(nhdsWithin x (Set.range f)).NeBot
source
theorem mem_closure_pi {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → TopologicalSpace (α i)] {I : Set ι} {s : (i : ι) → Set (α i)} {x : (i : ι) → α i} :
x ∈ closure (I.pi s) ↔ ∀ i ∈ I, x i ∈ closure (s i)
source
theorem closure_pi_set {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → TopologicalSpace (α i)] (I : Set ι) (s : (i : ι) → Set (α i)) :
closure (I.pi s) = I.pi fun (i : ι) => closure (s i)
source
theorem dense_pi {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → TopologicalSpace (α i)] {s : (i : ι) → Set (α i)} (I : Set ι) (hs : ∀ i ∈ I, Dense (s i)) :
Dense (I.pi s)
source
theorem DenseRange.piMap {ι : Type u_5} {X : ι → Type u_6} {Y : ι → Type u_7} [(i : ι) → TopologicalSpace (Y i)] {f : (i : ι) → X i → Y i} (hf : ∀ (i : ι), DenseRange (f i)) :
DenseRange (Pi.map f)
source
theorem eventuallyEq_nhdsWithin_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f g : α → β} {s : Set α} {a : α} :
f =ᶠ[nhdsWithin a s] g ↔ ∀ᶠ (x : α) in nhds a, x ∈ s → f x = g x
source
theorem eventuallyEq_nhds_of_eventuallyEq_nhdsNE {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f g : α → β} {a : α} (h₁ : f =ᶠ[nhdsWithin a {a}ᶜ] g) (h₂ : f a = g a) :
f =ᶠ[nhds a] g

Two functions agree on a neighborhood of `x` if they agree at `x` and in a punctured neighborhood.

source
theorem eventuallyEq_nhdsWithin_of_eqOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f g : α → β} {s : Set α} {a : α} (h : Set.EqOn f g s) :
f =ᶠ[nhdsWithin a s] g
source
theorem Set.EqOn.eventuallyEq_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f g : α → β} {s : Set α} {a : α} (h : EqOn f g s) :
f =ᶠ[nhdsWithin a s] g
source
theorem tendsto_nhdsWithin_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f g : α → β} {s : Set α} {a : α} {l : Filter β} (hfg : ∀ x ∈ s, f x = g x) (hf : Filter.Tendsto f (nhdsWithin a s) l) :
Filter.Tendsto g (nhdsWithin a s) l
source
theorem eventually_nhdsWithin_of_forall {α : Type u_1} [TopologicalSpace α] {s : Set α} {a : α} {p : α → Prop} (h : ∀ x ∈ s, p x) :
∀ᶠ (x : α) in nhdsWithin a s, p x
source
theorem tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {a : α} {l : Filter β} {s : Set α} (f : β → α) (h1 : Filter.Tendsto f l (nhds a)) (h2 : ∀ᶠ (x : β) in l, f x ∈ s) :
Filter.Tendsto f l (nhdsWithin a s)
source
theorem tendsto_nhdsWithin_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {a : α} {l : Filter β} {s : Set α} {f : β → α} :
Filter.Tendsto f l (nhdsWithin a s) ↔ Filter.Tendsto f l (nhds a) ∧ ∀ᶠ (n : β) in l, f n ∈ s
source
@[simp]
theorem tendsto_nhdsWithin_range {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {a : α} {l : Filter β} {f : β → α} :
Filter.Tendsto f l (nhdsWithin a (Set.range f)) ↔ Filter.Tendsto f l (nhds a)
source
theorem Filter.EventuallyEq.eq_of_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {s : Set α} {f g : α → β} {a : α} (h : f =ᶠ[nhdsWithin a s] g) (hmem : a ∈ s) :
f a = g a
source
theorem eventually_nhdsWithin_of_eventually_nhds {α : Type u_1} [TopologicalSpace α] {s : Set α} {a : α} {p : α → Prop} (h : ∀ᶠ (x : α) in nhds a, p x) :
∀ᶠ (x : α) in nhdsWithin a s, p x
source
theorem Set.MapsTo.preimage_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → β} {s : Set α} {t : Set β} {x : α} (hst : MapsTo f s t) :
f ⁻¹' t ∈ nhdsWithin x s

### `nhdsWithin` and subtypes #

source
theorem mem_nhdsWithin_subtype {α : Type u_1} [TopologicalSpace α] {s : Set α} {a : { x : α // x ∈ s }} {t u : Set { x : α // x ∈ s }} :
t ∈ nhdsWithin a u ↔ t ∈ Filter.comap Subtype.val (nhdsWithin (↑a) (Subtype.val '' u))
source
theorem nhdsWithin_subtype {α : Type u_1} [TopologicalSpace α] (s : Set α) (a : { x : α // x ∈ s }) (t : Set { x : α // x ∈ s }) :
nhdsWithin a t = Filter.comap Subtype.val (nhdsWithin (↑a) (Subtype.val '' t))
source
theorem nhdsWithin_eq_map_subtype_coe {α : Type u_1} [TopologicalSpace α] {s : Set α} {a : α} (h : a ∈ s) :
nhdsWithin a s = Filter.map Subtype.val (nhds ⟨a, h⟩)
source
theorem mem_nhds_subtype_iff_nhdsWithin {α : Type u_1} [TopologicalSpace α] {s : Set α} {a : ↑s} {t : Set ↑s} :
t ∈ nhds a ↔ Subtype.val '' t ∈ nhdsWithin (↑a) s
source
theorem preimage_coe_mem_nhds_subtype {α : Type u_1} [TopologicalSpace α] {s t : Set α} {a : ↑s} :
Subtype.val ⁻¹' t ∈ nhds a ↔ t ∈ nhdsWithin (↑a) s
source
theorem eventually_nhds_subtype_iff {α : Type u_1} [TopologicalSpace α] (s : Set α) (a : ↑s) (P : α → Prop) :
(∀ᶠ (x : ↑s) in nhds a, P ↑x) ↔ ∀ᶠ (x : α) in nhdsWithin (↑a) s, P x
source
theorem frequently_nhds_subtype_iff {α : Type u_1} [TopologicalSpace α] (s : Set α) (a : ↑s) (P : α → Prop) :
(∃ᶠ (x : ↑s) in nhds a, P ↑x) ↔ ∃ᶠ (x : α) in nhdsWithin (↑a) s, P x
source
theorem tendsto_nhdsWithin_iff_subtype {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {s : Set α} {a : α} (h : a ∈ s) (f : α → β) (l : Filter β) :
Filter.Tendsto f (nhdsWithin a s) l ↔ Filter.Tendsto (s.restrict f) (nhds ⟨a, h⟩) l