Neighborhoods relative to a subset

This file develops API on the relative versions nhdsWithin and nhdsSetWithin of nhds and nhdsSet, which are 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 relative 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;
• 𝓝ˢ[t] s: the filter nhdsSetWithin s t of neighborhoods of a set s within a set t.

Properties of the neighborhood-within filter

@[simp]

theorem nhds_bind_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} : ((nhds a).bind fun (x : α) => nhdsWithin x s) = nhdsWithin a s

@[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

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

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

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

@[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

@[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

theorem nhdsWithin_eq {α : Type u_1} [TopologicalSpace α] (a : α) (s : Set α) : nhdsWithin a s = ⨅ t ∈ {t : Set α | a ∈ t ∧ IsOpen t}, Filter.principal (t ∩ s)

@[simp]

theorem nhdsWithin_univ {α : Type u_1} [TopologicalSpace α] (a : α) : nhdsWithin a Set.univ = nhds a

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

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

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

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

theorem diff_mem_nhdsWithin_compl {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} (hs : s ∈ nhds x) (t : Set α) : s \ t ∈ nhdsWithin x tᶜ

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')

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

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

theorem mem_nhdsWithin_iff_eventuallyEq {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} : t ∈ nhdsWithin x s ↔ s =ᶠ[nhds x] s ∩ t

theorem mem_nhdsWithin_inter_self {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} : t ∈ nhdsWithin x (s ∩ t)

theorem mem_nhdsWithin_self_inter {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} : s ∈ nhdsWithin x (s ∩ t)

theorem nhdsWithin_eq_iff_eventuallyEq {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} : nhdsWithin x s = nhdsWithin x t ↔ s =ᶠ[nhds x] t

theorem nhdsWithin_le_iff {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} : nhdsWithin x s ≤ nhdsWithin x t ↔ t ∈ nhdsWithin x s

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

theorem mem_nhdsWithin_of_mem_nhds {α : Type u_1} [TopologicalSpace α] {s t : Set α} {a : α} (h : s ∈ nhds a) : s ∈ nhdsWithin a t

theorem self_mem_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} : s ∈ nhdsWithin a s

theorem eventually_mem_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} : ∀ᶠ (x : α) in nhdsWithin a s, x ∈ s

theorem inter_mem_nhdsWithin {α : Type u_1} [TopologicalSpace α] (s : Set α) {t : Set α} {a : α} (h : t ∈ nhds a) : s ∩ t ∈ nhdsWithin a s

theorem pure_le_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} (ha : a ∈ s) : pure a ≤ nhdsWithin a s

theorem mem_of_mem_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s t : Set α} (ha : a ∈ s) (ht : t ∈ nhdsWithin a s) : a ∈ t

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

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)

theorem nhdsWithin_restrict'' {α : Type u_1} [TopologicalSpace α] {a : α} (s : Set α) {t : Set α} (h : t ∈ nhdsWithin a s) : nhdsWithin a s = nhdsWithin a (s ∩ t)

theorem nhdsWithin_restrict' {α : Type u_1} [TopologicalSpace α] {a : α} (s : Set α) {t : Set α} (h : t ∈ nhds a) : nhdsWithin a s = nhdsWithin a (s ∩ t)

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)

theorem nhdsWithin_le_of_mem {α : Type u_1} [TopologicalSpace α] {a : α} {s t : Set α} (h : s ∈ nhdsWithin a t) : nhdsWithin a t ≤ nhdsWithin a s

theorem nhdsWithin_le_nhds {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} : nhdsWithin a s ≤ nhds a

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

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

@[simp]

theorem nhdsWithin_eq_nhds {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} : nhdsWithin a s = nhds a ↔ s ∈ nhds a

theorem IsOpen.nhdsWithin_eq {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} (h : IsOpen s) (ha : a ∈ s) : nhdsWithin a s = nhds a

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

@[simp]

theorem nhdsWithin_empty {α : Type u_1} [TopologicalSpace α] (a : α) : nhdsWithin a ∅ = ⊥

theorem nhdsWithin_union {α : Type u_1} [TopologicalSpace α] (a : α) (s t : Set α) : nhdsWithin a (s ∪ t) = nhdsWithin a s ⊔ nhdsWithin a t

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₂

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.

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.

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.

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)

theorem nhdsWithin_sUnion {α : Type u_1} [TopologicalSpace α] {S : Set (Set α)} (hS : S.Finite) (a : α) : nhdsWithin a (⋃₀ S) = ⨆ s ∈ S, nhdsWithin a s

theorem nhdsWithin_iUnion {α : Type u_1} [TopologicalSpace α] {ι : Sort u_5} [Finite ι] (s : ι → Set α) (a : α) : nhdsWithin a (⋃ (i : ι), s i) = ⨆ (i : ι), nhdsWithin a (s i)

theorem nhdsWithin_inter {α : Type u_1} [TopologicalSpace α] (a : α) (s t : Set α) : nhdsWithin a (s ∩ t) = nhdsWithin a s ⊓ nhdsWithin a t

theorem nhdsWithin_inter' {α : Type u_1} [TopologicalSpace α] (a : α) (s t : Set α) : nhdsWithin a (s ∩ t) = nhdsWithin a s ⊓ Filter.principal t

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

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

@[simp]

theorem nhdsWithin_singleton {α : Type u_1} [TopologicalSpace α] (a : α) : nhdsWithin a {a} = pure a

@[simp]

theorem nhdsWithin_insert {α : Type u_1} [TopologicalSpace α] (a : α) (s : Set α) : nhdsWithin a (insert a s) = pure a ⊔ nhdsWithin a s

theorem mem_nhdsWithin_insert {α : Type u_1} [TopologicalSpace α] {a : α} {s t : Set α} : t ∈ nhdsWithin a (insert a s) ↔ a ∈ t ∧ t ∈ nhdsWithin a s

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)

theorem insert_mem_nhds_iff {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} : insert a s ∈ nhds a ↔ s ∈ nhdsWithin a {a}ᶜ

@[simp]

theorem nhdsNE_sup_pure {α : Type u_1} [TopologicalSpace α] (a : α) : nhdsWithin a {a}ᶜ ⊔ pure a = nhds a

@[simp]

theorem pure_sup_nhdsNE {α : Type u_1} [TopologicalSpace α] (a : α) : pure a ⊔ nhdsWithin a {a}ᶜ = nhds a

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))

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)

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

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

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))

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))

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))

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) = ⊥

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

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

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

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

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

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

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))

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

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)

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

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

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)

theorem nhdsWithin_neBot_of_mem {α : Type u_1} [TopologicalSpace α] {s : Set α} {x : α} (hx : x ∈ s) : (nhdsWithin x s).NeBot

theorem IsClosed.mem_of_nhdsWithin_neBot {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : IsClosed s) {x : α} (hx : (nhdsWithin x s).NeBot) : x ∈ s

theorem DenseRange.nhdsWithin_neBot {α : Type u_1} [TopologicalSpace α] {ι : Type u_5} {f : ι → α} (h : DenseRange f) (x : α) : (nhdsWithin x (Set.range f)).NeBot

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)

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)

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)

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)

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

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.

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

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

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

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

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)

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

@[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)

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

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

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

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))

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))

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⟩)

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

theorem preimage_coe_mem_nhds_subtype {α : Type u_1} [TopologicalSpace α] {s t : Set α} {a : ↑s} : Subtype.val ⁻¹' t ∈ nhds a ↔ t ∈ nhdsWithin (↑a) s

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

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

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

The nhdsSetWithin-filter

theorem nhdsSetWithin_mono_left {α : Type u_1} [TopologicalSpace α] {s s' t : Set α} (h : s ⊆ s') : nhdsSetWithin s t ≤ nhdsSetWithin s' t

theorem nhdsSetWithin_mono_right {α : Type u_1} [TopologicalSpace α] {s t t' : Set α} (h : t ⊆ t') : nhdsSetWithin s t ≤ nhdsSetWithin s t'

theorem nhdsSetWithin_hasBasis {α : Type u_1} [TopologicalSpace α] {ι : Sort u_5} {p : ι → Prop} {s' : ι → Set α} {s : Set α} (h : (nhdsSet s).HasBasis p s') (t : Set α) : (nhdsSetWithin s t).HasBasis p fun (i : ι) => s' i ∩ t

theorem nhdsSetWithin_basis_open {α : Type u_1} [TopologicalSpace α] (s t : Set α) : (nhdsSetWithin s t).HasBasis (fun (u : Set α) => IsOpen u ∧ s ⊆ u) fun (u : Set α) => u ∩ t

theorem mem_nhdsSetWithin {α : Type u_1} [TopologicalSpace α] {s t u : Set α} : u ∈ nhdsSetWithin s t ↔ ∃ (v : Set α), IsOpen v ∧ s ⊆ v ∧ v ∩ t ⊆ u

@[simp]

theorem nhdsSetWithin_singleton {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} : nhdsSetWithin {x} s = nhdsWithin x s

@[simp]

theorem nhdsSetWithin_univ {α : Type u_1} [TopologicalSpace α] {s : Set α} : nhdsSetWithin s Set.univ = nhdsSet s

@[simp]

theorem nhdsSetWithin_univ' {α : Type u_1} [TopologicalSpace α] {s : Set α} : nhdsSetWithin Set.univ s = Filter.principal s

@[simp]

theorem nhdsSetWithin_self {α : Type u_1} [TopologicalSpace α] {s : Set α} : nhdsSetWithin s s = Filter.principal s

theorem nhdsSetWithin_eq_principal_of_subset {α : Type u_1} [TopologicalSpace α] {s t : Set α} (h : t ⊆ s) : nhdsSetWithin s t = Filter.principal t

@[simp]

theorem nhdsSetWithin_empty {α : Type u_1} [TopologicalSpace α] {s : Set α} : nhdsSetWithin s ∅ = ⊥

@[simp]

theorem nhdsSetWithin_empty' {α : Type u_1} [TopologicalSpace α] {s : Set α} : nhdsSetWithin ∅ s = ⊥

theorem principal_inter_le_nhdsSetWithin {α : Type u_1} [TopologicalSpace α] {s t : Set α} : Filter.principal (s ∩ t) ≤ nhdsSetWithin s t

theorem nhdsSetWithin_prod_le {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s s' : Set α} {t t' : Set β} : nhdsSetWithin (s ×ˢ t) (s' ×ˢ t') ≤ nhdsSetWithin s s' ×ˢ nhdsSetWithin t t'

theorem mem_nhdsSet_induced {α : Type u_5} {β : Type u_6} {t : TopologicalSpace β} (f : α → β) (s u : Set α) : u ∈ nhdsSet s ↔ ∃ v ∈ nhdsSet (f '' s), f ⁻¹' v ⊆ u

theorem nhdsSet_induced {α : Type u_5} {β : Type u_6} {t : TopologicalSpace β} (f : α → β) (s : Set α) : nhdsSet s = Filter.comap f (nhdsSet (f '' s))

theorem map_nhdsSet_induced_eq {α : Type u_5} {β : Type u_6} {t : TopologicalSpace β} {f : α → β} (s : Set α) : Filter.map f (nhdsSet s) = nhdsSetWithin (f '' s) (Set.range f)

theorem Topology.IsInducing.map_nhdsSet_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : IsInducing f) (s : Set α) : Filter.map f (nhdsSet s) = nhdsSetWithin (f '' s) (Set.range f)

theorem map_nhdsSet_subtype_val {α : Type u_1} [TopologicalSpace α] {s : Set α} (t : Set ↑s) : Filter.map Subtype.val (nhdsSet t) = nhdsSetWithin (Subtype.val '' t) s

theorem mem_nhdsSet_subtype_iff_nhdsSetWithin {α : Type u_1} [TopologicalSpace α] {s : Set α} {t u : Set ↑s} : u ∈ nhdsSet t ↔ Subtype.val '' u ∈ nhdsSetWithin (Subtype.val '' t) s