Neighborhoods and continuity relative to a subset

This file defines relative versions

• nhdsWithin of nhds
• ContinuousOn of Continuous
• ContinuousWithinAt of ContinuousAt

and proves their basic properties, including the relationships between these restricted notions and the corresponding notions for the subtype equipped with the subspace topology.

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.

@[simp]

theorem nhds_bind_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} : (Filter.bind (nhds a) 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_nhdsWithin_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

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

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

theorem nhdsWithin_hasBasis {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {p : β → Prop} {s : β → Set α} {a : α} (h : Filter.HasBasis (nhds a) p s) (t : Set α) : Filter.HasBasis (nhdsWithin a t) p fun i => s i ∩ t

theorem nhdsWithin_basis_open {α : Type u_1} [TopologicalSpace α] (a : α) (t : Set α) : Filter.HasBasis (nhdsWithin a t) (fun u => a ∈ u ∧ IsOpen u) fun u => u ∩ t

theorem mem_nhdsWithin {α : Type u_1} [TopologicalSpace α] {t : Set α} {a : α} {s : Set α} : t ∈ nhdsWithin a s ↔ ∃ u, 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, 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 : Set α} {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 : Set α} {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 : Set α} {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 : Set α} {t : Set α} {x : α} : t ∈ nhdsWithin x s ↔ s =ᶠ[nhds x] s ∩ t

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

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

theorem preimage_nhdsWithin_coinduced' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {π : α → β} {s : Set β} {t : Set α} {a : α} (h : a ∈ t) (hs : s ∈ nhds (π a)) : π ⁻¹' s ∈ nhdsWithin a t

theorem mem_nhdsWithin_of_mem_nhds {α : Type u_1} [TopologicalSpace α] {s : Set α} {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 nhdsWithin_mono {α : Type u_1} [TopologicalSpace α] (a : α) {s : Set α} {t : Set α} (h : s ⊆ t) : nhdsWithin a s ≤ nhdsWithin a t

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 : Set α} {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 : Set α} {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 : Set α} {t : Set α} {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 : Set α} {t : Set α} {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 α] {π : α → β} {s : Set β} {t : Set α} {a : α} (h : a ∈ t) (ht : IsOpen t) (hs : s ∈ nhds (π a)) : π ⁻¹' s ∈ nhds a

@[simp]

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

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

theorem nhdsWithin_biUnion {α : Type u_1} [TopologicalSpace α] {ι : Type u_5} {I : Set ι} (hI : Set.Finite I) (s : ι → Set α) (a : α) : nhdsWithin a (⋃ (i : ι) (_ : i ∈ I), s i) = ⨆ (i : ι) (_ : i ∈ I), nhdsWithin a (s i)

theorem nhdsWithin_sUnion {α : Type u_1} [TopologicalSpace α] {S : Set (Set α)} (hS : Set.Finite S) (a : α) : nhdsWithin a (⋃₀ S) = ⨆ (s : Set α) (_ : 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 : Set α) (t : Set α) : nhdsWithin a (s ∩ t) = nhdsWithin a s ⊓ nhdsWithin a t

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

theorem nhdsWithin_inter_of_mem {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {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 : Set α} {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 : Set α} {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 : Set α} {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 nhdsWithin_compl_singleton_sup_pure {α : Type u_1} [TopologicalSpace α] (a : α) : nhdsWithin a {a}ᶜ ⊔ pure a = nhds a

theorem nhdsWithin_prod {α : Type u_5} [TopologicalSpace α] {β : Type u_6} [TopologicalSpace β] {s : Set α} {u : Set α} {t : Set β} {v : Set β} {a : α} {b : β} (hu : u ∈ nhdsWithin a s) (hv : v ∈ nhdsWithin b t) : u ×ˢ v ∈ nhdsWithin (a, b) (s ×ˢ t)

theorem nhdsWithin_pi_eq' {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → TopologicalSpace (α i)] {I : Set ι} (hI : Set.Finite I) (s : (i : ι) → Set (α i)) (x : (i : ι) → α i) : nhdsWithin x (Set.pi I s) = ⨅ (i : ι), Filter.comap (fun x => x i) (nhds (x i) ⊓ ⨅ (_ : i ∈ I), Filter.principal (s i))

theorem nhdsWithin_pi_eq {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → TopologicalSpace (α i)] {I : Set ι} (hI : Set.Finite I) (s : (i : ι) → Set (α i)) (x : (i : ι) → α i) : nhdsWithin x (Set.pi I s) = (⨅ (i : ι) (_ : i ∈ I), Filter.comap (fun x => x i) (nhdsWithin (x i) (s i))) ⊓ ⨅ (i : ι) (_ : ¬i ∈ I), Filter.comap (fun x => x i) (nhds (x i))

theorem nhdsWithin_pi_univ_eq {ι : Type u_5} {α : ι → Type u_6} [Finite ι] [(i : ι) → TopologicalSpace (α i)] (s : (i : ι) → Set (α i)) (x : (i : ι) → α i) : nhdsWithin x (Set.pi Set.univ s) = ⨅ (i : ι), Filter.comap (fun x => x i) (nhdsWithin (x i) (s i))

theorem nhdsWithin_pi_eq_bot {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → TopologicalSpace (α i)] {I : Set ι} {s : (i : ι) → Set (α i)} {x : (i : ι) → α i} : nhdsWithin x (Set.pi I s) = ⊥ ↔ ∃ i, i ∈ I ∧ nhdsWithin (x i) (s i) = ⊥

theorem nhdsWithin_pi_neBot {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → TopologicalSpace (α i)] {I : Set ι} {s : (i : ι) → Set (α i)} {x : (i : ι) → α i} : Filter.NeBot (nhdsWithin x (Set.pi I s)) ↔ ∀ (i : ι), i ∈ I → Filter.NeBot (nhdsWithin (x i) (s i))

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₀ : Filter.Tendsto f (nhdsWithin a (s ∩ t)) l) (h₁ : Filter.Tendsto g (nhdsWithin a (s ∩ tᶜ)) l) : Filter.Tendsto (Set.piecewise t 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₀ : Filter.Tendsto f (nhdsWithin a (s ∩ {x | p x})) l) (h₁ : Filter.Tendsto g (nhdsWithin a (s ∩ {x | ¬p x})) l) : Filter.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 : Set α) (_ : t ∈ {t | a ∈ t ∧ IsOpen t}), Filter.principal (f '' (t ∩ s))

theorem tendsto_nhdsWithin_mono_left {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → β} {a : α} {s : Set α} {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 : Set α} {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 principal_subtype {α : Type u_5} (s : Set α) (t : Set ↑s) : Filter.principal t = Filter.comap Subtype.val (Filter.principal (Subtype.val '' t))

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

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

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

theorem mem_closure_pi {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → TopologicalSpace (α i)] {I : Set ι} {s : (i : ι) → Set (α i)} {x : (i : ι) → α i} : x ∈ closure (Set.pi I s) ↔ ∀ (i : ι), 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 (Set.pi I s) = Set.pi I 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 ∈ I → Dense (s i)) : Dense (Set.pi I s)

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_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 : Set.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 : α), 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 : α) → 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_5} [TopologicalSpace α] {s : Set α} {a : α} {p : α → Prop} (h : ∀ᶠ (x : α) in nhds a, p x) : ∀ᶠ (x : α) in nhdsWithin a s, p x

nhdsWithin and subtypes

theorem mem_nhdsWithin_subtype {α : Type u_1} [TopologicalSpace α] {s : Set α} {a : { x // x ∈ s }} {t : Set { x // x ∈ s }} {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 { val := a, property := 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 : Set α} {t : Set α} {a : ↑s} : Subtype.val ⁻¹' t ∈ nhds a ↔ t ∈ nhdsWithin (↑a) s

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 (Set.restrict s f) (nhds { val := a, property := h }) l

def ContinuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (s : Set α) (x : α) : Prop

A function between topological spaces is continuous at a point x₀ within a subset s if f x tends to f x₀ when x tends to x₀ while staying within s.

Equations

• ContinuousWithinAt f s x = Filter.Tendsto f (nhdsWithin x s) (nhds (f x))

theorem ContinuousWithinAt.tendsto {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) : Filter.Tendsto f (nhdsWithin x s) (nhds (f x))

If a function is continuous within s at x, then it tends to f x within s by definition. We register this fact for use with the dot notation, especially to use Filter.Tendsto.comp as ContinuousWithinAt.comp will have a different meaning.

def ContinuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (s : Set α) : Prop

A function between topological spaces is continuous on a subset s when it's continuous at every point of s within s.

Equations

• ContinuousOn f s = ∀ (x : α), x ∈ s → ContinuousWithinAt f s x

theorem ContinuousOn.continuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} (hf : ContinuousOn f s) (hx : x ∈ s) : ContinuousWithinAt f s x

theorem continuousWithinAt_univ {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (x : α) : ContinuousWithinAt f Set.univ x ↔ ContinuousAt f x

theorem continuousWithinAt_iff_continuousAt_restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) {x : α} {s : Set α} (h : x ∈ s) : ContinuousWithinAt f s x ↔ ContinuousAt (Set.restrict s f) { val := x, property := h }

theorem ContinuousWithinAt.tendsto_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} {s : Set α} {t : Set β} (h : ContinuousWithinAt f s x) (ht : Set.MapsTo f s t) : Filter.Tendsto f (nhdsWithin x s) (nhdsWithin (f x) t)

theorem ContinuousWithinAt.tendsto_nhdsWithin_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} {s : Set α} (h : ContinuousWithinAt f s x) : Filter.Tendsto f (nhdsWithin x s) (nhdsWithin (f x) (f '' s))

theorem ContinuousWithinAt.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {f : α → γ} {g : β → δ} {s : Set α} {t : Set β} {x : α} {y : β} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g t y) : ContinuousWithinAt (Prod.map f g) (s ×ˢ t) (x, y)

theorem continuousWithinAt_pi {α : Type u_1} [TopologicalSpace α] {ι : Type u_5} {π : ι → Type u_6} [(i : ι) → TopologicalSpace (π i)] {f : α → (i : ι) → π i} {s : Set α} {x : α} : ContinuousWithinAt f s x ↔ ∀ (i : ι), ContinuousWithinAt (fun y => f y i) s x

theorem continuousOn_pi {α : Type u_1} [TopologicalSpace α] {ι : Type u_5} {π : ι → Type u_6} [(i : ι) → TopologicalSpace (π i)] {f : α → (i : ι) → π i} {s : Set α} : ContinuousOn f s ↔ ∀ (i : ι), ContinuousOn (fun y => f y i) s

theorem ContinuousWithinAt.fin_insertNth {α : Type u_1} [TopologicalSpace α] {n : ℕ} {π : Fin (n + 1) → Type u_5} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : α → π i} {a : α} {s : Set α} (hf : ContinuousWithinAt f s a) {g : α → (j : Fin n) → π (Fin.succAbove i j)} (hg : ContinuousWithinAt g s a) : ContinuousWithinAt (fun a => Fin.insertNth i (f a) (g a)) s a

theorem ContinuousOn.fin_insertNth {α : Type u_1} [TopologicalSpace α] {n : ℕ} {π : Fin (n + 1) → Type u_5} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : α → π i} {s : Set α} (hf : ContinuousOn f s) {g : α → (j : Fin n) → π (Fin.succAbove i j)} (hg : ContinuousOn g s) : ContinuousOn (fun a => Fin.insertNth i (f a) (g a)) s

theorem continuousOn_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} : ContinuousOn f s ↔ ∀ (x : α), x ∈ s → ∀ (t : Set β), IsOpen t → f x ∈ t → ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ s ⊆ f ⁻¹' t

theorem continuousOn_iff_continuous_restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} : ContinuousOn f s ↔ Continuous (Set.restrict s f)

theorem ContinuousOn.restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} : ContinuousOn f s → Continuous (Set.restrict s f)

Alias of the forward direction of continuousOn_iff_continuous_restrict.

theorem ContinuousOn.restrict_mapsTo {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {t : Set β} (hf : ContinuousOn f s) (ht : Set.MapsTo f s t) : Continuous (Set.MapsTo.restrict f s t ht)

theorem continuousOn_iff' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} : ContinuousOn f s ↔ ∀ (t : Set β), IsOpen t → ∃ u, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s

theorem ContinuousOn.mono_dom {α : Type u_5} {β : Type u_6} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} (h₁ : t₂ ≤ t₁) {s : Set α} {f : α → β} (h₂ : ContinuousOn f s) : ContinuousOn f s

If a function is continuous on a set for some topologies, then it is continuous on the same set with respect to any finer topology on the source space.

theorem ContinuousOn.mono_rng {α : Type u_5} {β : Type u_6} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β} {t₃ : TopologicalSpace β} (h₁ : t₂ ≤ t₃) {s : Set α} {f : α → β} (h₂ : ContinuousOn f s) : ContinuousOn f s

If a function is continuous on a set for some topologies, then it is continuous on the same set with respect to any coarser topology on the target space.

theorem continuousOn_iff_isClosed {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} : ContinuousOn f s ↔ ∀ (t : Set β), IsClosed t → ∃ u, IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s

theorem ContinuousOn.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {f : α → γ} {g : β → δ} {s : Set α} {t : Set β} (hf : ContinuousOn f s) (hg : ContinuousOn g t) : ContinuousOn (Prod.map f g) (s ×ˢ t)

theorem continuous_of_cover_nhds {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {ι : Sort u_5} {f : α → β} {s : ι → Set α} (hs : ∀ (x : α), ∃ i, s i ∈ nhds x) (hf : ∀ (i : ι), ContinuousOn f (s i)) : Continuous f

theorem continuousOn_empty {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) : ContinuousOn f ∅

theorem continuousOn_singleton {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (a : α) : ContinuousOn f {a}

theorem Set.Subsingleton.continuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} (hs : Set.Subsingleton s) (f : α → β) : ContinuousOn f s

theorem nhdsWithin_le_comap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {x : α} {s : Set α} {f : α → β} (ctsf : ContinuousWithinAt f s x) : nhdsWithin x s ≤ Filter.comap f (nhdsWithin (f x) (f '' s))

@[simp]

theorem comap_nhdsWithin_range {β : Type u_2} [TopologicalSpace β] {α : Type u_5} (f : α → β) (y : β) : Filter.comap f (nhdsWithin y (Set.range f)) = Filter.comap f (nhds y)

theorem continuous_iff_continuousOn_univ {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} : Continuous f ↔ ContinuousOn f Set.univ

theorem ContinuousWithinAt.mono {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {t : Set α} {x : α} (h : ContinuousWithinAt f t x) (hs : s ⊆ t) : ContinuousWithinAt f s x

theorem ContinuousWithinAt.mono_of_mem {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {t : Set α} {x : α} (h : ContinuousWithinAt f t x) (hs : t ∈ nhdsWithin x s) : ContinuousWithinAt f s x

theorem continuousWithinAt_congr_nhds {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {x : α} {s : Set α} {t : Set α} {f : α → β} (h : nhdsWithin x s = nhdsWithin x t) : ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x

theorem continuousWithinAt_inter' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {t : Set α} {x : α} (h : t ∈ nhdsWithin x s) : ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x

theorem continuousWithinAt_inter {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {t : Set α} {x : α} (h : t ∈ nhds x) : ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x

theorem continuousWithinAt_union {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {t : Set α} {x : α} : ContinuousWithinAt f (s ∪ t) x ↔ ContinuousWithinAt f s x ∧ ContinuousWithinAt f t x

theorem ContinuousWithinAt.union {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {t : Set α} {x : α} (hs : ContinuousWithinAt f s x) (ht : ContinuousWithinAt f t x) : ContinuousWithinAt f (s ∪ t) x

theorem ContinuousWithinAt.mem_closure_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) (hx : x ∈ closure s) : f x ∈ closure (f '' s)

theorem ContinuousWithinAt.mem_closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} {A : Set β} (h : ContinuousWithinAt f s x) (hx : x ∈ closure s) (hA : Set.MapsTo f s A) : f x ∈ closure A

theorem Set.MapsTo.closure_of_continuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {t : Set β} (h : Set.MapsTo f s t) (hc : ∀ (x : α), x ∈ closure s → ContinuousWithinAt f s x) : Set.MapsTo f (closure s) (closure t)

theorem Set.MapsTo.closure_of_continuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {t : Set β} (h : Set.MapsTo f s t) (hc : ContinuousOn f (closure s)) : Set.MapsTo f (closure s) (closure t)

theorem ContinuousWithinAt.image_closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (hf : ∀ (x : α), x ∈ closure s → ContinuousWithinAt f s x) : f '' closure s ⊆ closure (f '' s)

theorem ContinuousOn.image_closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (hf : ContinuousOn f (closure s)) : f '' closure s ⊆ closure (f '' s)

@[simp]

theorem continuousWithinAt_singleton {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} : ContinuousWithinAt f {x} x

@[simp]

theorem continuousWithinAt_insert_self {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} {s : Set α} : ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x

theorem ContinuousWithinAt.insert_self {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} {s : Set α} : ContinuousWithinAt f s x → ContinuousWithinAt f (insert x s) x

Alias of the reverse direction of continuousWithinAt_insert_self.

theorem ContinuousWithinAt.diff_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {t : Set α} {x : α} (ht : ContinuousWithinAt f t x) : ContinuousWithinAt f (s \ t) x ↔ ContinuousWithinAt f s x

@[simp]

theorem continuousWithinAt_diff_self {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} : ContinuousWithinAt f (s \ {x}) x ↔ ContinuousWithinAt f s x

@[simp]

theorem continuousWithinAt_compl_self {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {a : α} : ContinuousWithinAt f {a}ᶜ a ↔ ContinuousAt f a

@[simp]

theorem continuousWithinAt_update_same {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [DecidableEq α] {f : α → β} {s : Set α} {x : α} {y : β} : ContinuousWithinAt (Function.update f x y) s x ↔ Filter.Tendsto f (nhdsWithin x (s \ {x})) (nhds y)

@[simp]

theorem continuousAt_update_same {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [DecidableEq α] {f : α → β} {x : α} {y : β} : ContinuousAt (Function.update f x y) x ↔ Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds y)

theorem IsOpenMap.continuousOn_image_of_leftInvOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (h : IsOpenMap (Set.restrict s f)) {finv : β → α} (hleft : Set.LeftInvOn finv f s) : ContinuousOn finv (f '' s)

theorem IsOpenMap.continuousOn_range_of_leftInverse {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : IsOpenMap f) {finv : β → α} (hleft : Function.LeftInverse finv f) : ContinuousOn finv (Set.range f)

theorem ContinuousOn.congr_mono {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : α → β} {s : Set α} {s₁ : Set α} (h : ContinuousOn f s) (h' : Set.EqOn g f s₁) (h₁ : s₁ ⊆ s) : ContinuousOn g s₁

theorem ContinuousOn.congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : α → β} {s : Set α} (h : ContinuousOn f s) (h' : Set.EqOn g f s) : ContinuousOn g s

theorem continuousOn_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : α → β} {s : Set α} (h' : Set.EqOn g f s) : ContinuousOn g s ↔ ContinuousOn f s

theorem ContinuousAt.continuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} (h : ContinuousAt f x) : ContinuousWithinAt f s x

theorem continuousWithinAt_iff_continuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} (h : s ∈ nhds x) : ContinuousWithinAt f s x ↔ ContinuousAt f x

theorem ContinuousWithinAt.continuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) (hs : s ∈ nhds x) : ContinuousAt f x

theorem IsOpen.continuousOn_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (hs : IsOpen s) : ContinuousOn f s ↔ ∀ ⦃a : α⦄, a ∈ s → ContinuousAt f a

theorem ContinuousOn.continuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} (h : ContinuousOn f s) (hx : s ∈ nhds x) : ContinuousAt f x

theorem ContinuousAt.continuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (hcont : ∀ (x : α), x ∈ s → ContinuousAt f x) : ContinuousOn f s

theorem ContinuousWithinAt.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} {x : α} (hg : ContinuousWithinAt g t (f x)) (hf : ContinuousWithinAt f s x) (h : Set.MapsTo f s t) : ContinuousWithinAt (g ∘ f) s x

theorem ContinuousWithinAt.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} {x : α} (hg : ContinuousWithinAt g t (f x)) (hf : ContinuousWithinAt f s x) : ContinuousWithinAt (g ∘ f) (s ∩ f ⁻¹' t) x

theorem ContinuousAt.comp_continuousWithinAt {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set α} {x : α} (hg : ContinuousAt g (f x)) (hf : ContinuousWithinAt f s x) : ContinuousWithinAt (g ∘ f) s x

theorem ContinuousOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : ContinuousOn g t) (hf : ContinuousOn f s) (h : Set.MapsTo f s t) : ContinuousOn (g ∘ f) s

theorem ContinuousOn.mono {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {t : Set α} (hf : ContinuousOn f s) (h : t ⊆ s) : ContinuousOn f t

theorem antitone_continuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} : Antitone (ContinuousOn f)

theorem ContinuousOn.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set α} {t : Set β} (hg : ContinuousOn g t) (hf : ContinuousOn f s) : ContinuousOn (g ∘ f) (s ∩ f ⁻¹' t)

theorem Continuous.continuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (h : Continuous f) : ContinuousOn f s

theorem Continuous.continuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} (h : Continuous f) : ContinuousWithinAt f s x

theorem Continuous.comp_continuousOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set α} (hg : Continuous g) (hf : ContinuousOn f s) : ContinuousOn (g ∘ f) s

theorem ContinuousOn.comp_continuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set β} (hg : ContinuousOn g s) (hf : Continuous f) (hs : ∀ (x : α), f x ∈ s) : Continuous (g ∘ f)

theorem ContinuousWithinAt.preimage_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} {s : Set α} {t : Set β} (h : ContinuousWithinAt f s x) (ht : t ∈ nhds (f x)) : f ⁻¹' t ∈ nhdsWithin x s

theorem Set.LeftInvOn.map_nhdsWithin_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : β → α} {x : β} {s : Set β} (h : Set.LeftInvOn f g s) (hx : f (g x) = x) (hf : ContinuousWithinAt f (g '' s) (g x)) (hg : ContinuousWithinAt g s x) : Filter.map g (nhdsWithin x s) = nhdsWithin (g x) (g '' s)

theorem Function.LeftInverse.map_nhds_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : β → α} {x : β} (h : Function.LeftInverse f g) (hf : ContinuousWithinAt f (Set.range g) (g x)) (hg : ContinuousAt g x) : Filter.map g (nhds x) = nhdsWithin (g x) (Set.range g)

theorem ContinuousWithinAt.preimage_mem_nhdsWithin' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} {s : Set α} {t : Set β} (h : ContinuousWithinAt f s x) (ht : t ∈ nhdsWithin (f x) (f '' s)) : f ⁻¹' t ∈ nhdsWithin x s

theorem ContinuousWithinAt.preimage_mem_nhdsWithin'' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} {y : β} {s : Set β} {t : Set β} (h : ContinuousWithinAt f (f ⁻¹' s) x) (ht : t ∈ nhdsWithin y s) (hxy : y = f x) : f ⁻¹' t ∈ nhdsWithin x (f ⁻¹' s)

theorem Filter.EventuallyEq.congr_continuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : α → β} {s : Set α} {x : α} (h : f =ᶠ[nhdsWithin x s] g) (hx : f x = g x) : ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x

theorem ContinuousWithinAt.congr_of_eventuallyEq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {f₁ : α → β} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) (h₁ : f₁ =ᶠ[nhdsWithin x s] f) (hx : f₁ x = f x) : ContinuousWithinAt f₁ s x

theorem ContinuousWithinAt.congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {f₁ : α → β} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) (h₁ : ∀ (y : α), y ∈ s → f₁ y = f y) (hx : f₁ x = f x) : ContinuousWithinAt f₁ s x

theorem ContinuousWithinAt.congr_mono {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : α → β} {s : Set α} {s₁ : Set α} {x : α} (h : ContinuousWithinAt f s x) (h' : Set.EqOn g f s₁) (h₁ : s₁ ⊆ s) (hx : g x = f x) : ContinuousWithinAt g s₁ x

theorem continuousOn_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {c : β} : ContinuousOn (fun x => c) s

theorem continuousWithinAt_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {b : β} {s : Set α} {x : α} : ContinuousWithinAt (fun x => b) s x

theorem continuousOn_id {α : Type u_1} [TopologicalSpace α] {s : Set α} : ContinuousOn id s

theorem continuousWithinAt_id {α : Type u_1} [TopologicalSpace α] {s : Set α} {x : α} : ContinuousWithinAt id s x

theorem continuousOn_open_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (hs : IsOpen s) : ContinuousOn f s ↔ ∀ (t : Set β), IsOpen t → IsOpen (s ∩ f ⁻¹' t)

theorem ContinuousOn.preimage_open_of_open {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {t : Set β} (hf : ContinuousOn f s) (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s ∩ f ⁻¹' t)

theorem ContinuousOn.isOpen_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {t : Set β} (h : ContinuousOn f s) (hs : IsOpen s) (hp : f ⁻¹' t ⊆ s) (ht : IsOpen t) : IsOpen (f ⁻¹' t)

theorem ContinuousOn.preimage_closed_of_closed {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {t : Set β} (hf : ContinuousOn f s) (hs : IsClosed s) (ht : IsClosed t) : IsClosed (s ∩ f ⁻¹' t)

theorem ContinuousOn.preimage_interior_subset_interior_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {t : Set β} (hf : ContinuousOn f s) (hs : IsOpen s) : s ∩ f ⁻¹' interior t ⊆ s ∩ interior (f ⁻¹' t)

theorem continuousOn_of_locally_continuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (h : ∀ (x : α), x ∈ s → ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)) : ContinuousOn f s

theorem continuousOn_to_generateFrom_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {s : Set α} {T : Set (Set β)} {f : α → β} : ContinuousOn f s ↔ ∀ (x : α), x ∈ s → ∀ (t : Set β), t ∈ T → f x ∈ t → f ⁻¹' t ∈ nhdsWithin x s

theorem continuousOn_open_of_generateFrom {α : Type u_1} [TopologicalSpace α] {β : Type u_5} {s : Set α} {T : Set (Set β)} {f : α → β} (h : ∀ (t : Set β), t ∈ T → IsOpen (s ∩ f ⁻¹' t)) : ContinuousOn f s

theorem ContinuousWithinAt.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {g : α → γ} {s : Set α} {x : α} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) : ContinuousWithinAt (fun x => (f x, g x)) s x

theorem ContinuousOn.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {g : α → γ} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun x => (f x, g x)) s

theorem Inducing.continuousWithinAt_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {g : β → γ} (hg : Inducing g) {s : Set α} {x : α} : ContinuousWithinAt f s x ↔ ContinuousWithinAt (g ∘ f) s x

theorem Inducing.continuousOn_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {g : β → γ} (hg : Inducing g) {s : Set α} : ContinuousOn f s ↔ ContinuousOn (g ∘ f) s

theorem Embedding.continuousOn_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {g : β → γ} (hg : Embedding g) {s : Set α} : ContinuousOn f s ↔ ContinuousOn (g ∘ f) s

theorem Embedding.map_nhdsWithin_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Embedding f) (s : Set α) (x : α) : Filter.map f (nhdsWithin x s) = nhdsWithin (f x) (f '' s)

theorem OpenEmbedding.map_nhdsWithin_preimage_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : OpenEmbedding f) (s : Set β) (x : α) : Filter.map f (nhdsWithin x (f ⁻¹' s)) = nhdsWithin (f x) s

theorem continuousWithinAt_of_not_mem_closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} : ¬x ∈ closure s → ContinuousWithinAt f s x

theorem ContinuousOn.if' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {p : α → Prop} {f : α → β} {g : α → β} [(a : α) → Decidable (p a)] (hpf : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Filter.Tendsto f (nhdsWithin a (s ∩ {a | p a})) (nhds (if p a then f a else g a))) (hpg : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → Filter.Tendsto g (nhdsWithin a (s ∩ {a | ¬p a})) (nhds (if p a then f a else g a))) (hf : ContinuousOn f (s ∩ {a | p a})) (hg : ContinuousOn g (s ∩ {a | ¬p a})) : ContinuousOn (fun a => if p a then f a else g a) s

theorem ContinuousOn.piecewise' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set α} {f : α → β} {g : α → β} [(a : α) → Decidable (a ∈ t)] (hpf : ∀ (a : α), a ∈ s ∩ frontier t → Filter.Tendsto f (nhdsWithin a (s ∩ t)) (nhds (Set.piecewise t f g a))) (hpg : ∀ (a : α), a ∈ s ∩ frontier t → Filter.Tendsto g (nhdsWithin a (s ∩ tᶜ)) (nhds (Set.piecewise t f g a))) (hf : ContinuousOn f (s ∩ t)) (hg : ContinuousOn g (s ∩ tᶜ)) : ContinuousOn (Set.piecewise t f g) s

theorem ContinuousOn.if {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] {p : α → Prop} [(a : α) → Decidable (p a)] {s : Set α} {f : α → β} {g : α → β} (hp : ∀ (a : α), a ∈ s ∩ frontier {a | p a} → f a = g a) (hf : ContinuousOn f (s ∩ closure {a | p a})) (hg : ContinuousOn g (s ∩ closure {a | ¬p a})) : ContinuousOn (fun a => if p a then f a else g a) s

theorem ContinuousOn.piecewise {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set α} {f : α → β} {g : α → β} [(a : α) → Decidable (a ∈ t)] (ht : ∀ (a : α), a ∈ s ∩ frontier t → f a = g a) (hf : ContinuousOn f (s ∩ closure t)) (hg : ContinuousOn g (s ∩ closure tᶜ)) : ContinuousOn (Set.piecewise t f g) s

theorem continuous_if' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {p : α → Prop} {f : α → β} {g : α → β} [(a : α) → Decidable (p a)] (hpf : ∀ (a : α), a ∈ frontier {x | p x} → Filter.Tendsto f (nhdsWithin a {x | p x}) (nhds (if p a then f a else g a))) (hpg : ∀ (a : α), a ∈ frontier {x | p x} → Filter.Tendsto g (nhdsWithin a {x | ¬p x}) (nhds (if p a then f a else g a))) (hf : ContinuousOn f {x | p x}) (hg : ContinuousOn g {x | ¬p x}) : Continuous fun a => if p a then f a else g a

theorem continuous_if {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {p : α → Prop} {f : α → β} {g : α → β} [(a : α) → Decidable (p a)] (hp : ∀ (a : α), a ∈ frontier {x | p x} → f a = g a) (hf : ContinuousOn f (closure {x | p x})) (hg : ContinuousOn g (closure {x | ¬p x})) : Continuous fun a => if p a then f a else g a

theorem Continuous.if {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {p : α → Prop} {f : α → β} {g : α → β} [(a : α) → Decidable (p a)] (hp : ∀ (a : α), a ∈ frontier {x | p x} → f a = g a) (hf : Continuous f) (hg : Continuous g) : Continuous fun a => if p a then f a else g a

theorem continuous_if_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (p : Prop) {f : α → β} {g : α → β} [Decidable p] (hf : p → Continuous f) (hg : ¬p → Continuous g) : Continuous fun a => if p then f a else g a

theorem Continuous.if_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (p : Prop) {f : α → β} {g : α → β} [Decidable p] (hf : Continuous f) (hg : Continuous g) : Continuous fun a => if p then f a else g a

theorem continuous_piecewise {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : α → β} {g : α → β} [(a : α) → Decidable (a ∈ s)] (hs : ∀ (a : α), a ∈ frontier s → f a = g a) (hf : ContinuousOn f (closure s)) (hg : ContinuousOn g (closure sᶜ)) : Continuous (Set.piecewise s f g)

theorem Continuous.piecewise {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : α → β} {g : α → β} [(a : α) → Decidable (a ∈ s)] (hs : ∀ (a : α), a ∈ frontier s → f a = g a) (hf : Continuous f) (hg : Continuous g) : Continuous (Set.piecewise s f g)

theorem IsOpen.ite' {α : Type u_1} [TopologicalSpace α] {s : Set α} {s' : Set α} {t : Set α} (hs : IsOpen s) (hs' : IsOpen s') (ht : ∀ (x : α), x ∈ frontier t → (x ∈ s ↔ x ∈ s')) : IsOpen (Set.ite t s s')

theorem IsOpen.ite {α : Type u_1} [TopologicalSpace α] {s : Set α} {s' : Set α} {t : Set α} (hs : IsOpen s) (hs' : IsOpen s') (ht : s ∩ frontier t = s' ∩ frontier t) : IsOpen (Set.ite t s s')

theorem ite_inter_closure_eq_of_inter_frontier_eq {α : Type u_1} [TopologicalSpace α] {s : Set α} {s' : Set α} {t : Set α} (ht : s ∩ frontier t = s' ∩ frontier t) : Set.ite t s s' ∩ closure t = s ∩ closure t

theorem ite_inter_closure_compl_eq_of_inter_frontier_eq {α : Type u_1} [TopologicalSpace α] {s : Set α} {s' : Set α} {t : Set α} (ht : s ∩ frontier t = s' ∩ frontier t) : Set.ite t s s' ∩ closure tᶜ = s' ∩ closure tᶜ

theorem continuousOn_piecewise_ite' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {s' : Set α} {t : Set α} {f : α → β} {f' : α → β} [(x : α) → Decidable (x ∈ t)] (h : ContinuousOn f (s ∩ closure t)) (h' : ContinuousOn f' (s' ∩ closure tᶜ)) (H : s ∩ frontier t = s' ∩ frontier t) (Heq : Set.EqOn f f' (s ∩ frontier t)) : ContinuousOn (Set.piecewise t f f') (Set.ite t s s')

theorem continuousOn_piecewise_ite {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {s' : Set α} {t : Set α} {f : α → β} {f' : α → β} [(x : α) → Decidable (x ∈ t)] (h : ContinuousOn f s) (h' : ContinuousOn f' s') (H : s ∩ frontier t = s' ∩ frontier t) (Heq : Set.EqOn f f' (s ∩ frontier t)) : ContinuousOn (Set.piecewise t f f') (Set.ite t s s')

theorem frontier_inter_open_inter {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} (ht : IsOpen t) : frontier (s ∩ t) ∩ t = frontier s ∩ t

theorem continuousOn_fst {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set (α × β)} : ContinuousOn Prod.fst s

theorem continuousWithinAt_fst {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set (α × β)} {p : α × β} : ContinuousWithinAt Prod.fst s p

theorem ContinuousOn.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β × γ} {s : Set α} (hf : ContinuousOn f s) : ContinuousOn (fun x => (f x).fst) s

theorem ContinuousWithinAt.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β × γ} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) : ContinuousWithinAt (fun x => (f x).fst) s a

theorem continuousOn_snd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set (α × β)} : ContinuousOn Prod.snd s

theorem continuousWithinAt_snd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set (α × β)} {p : α × β} : ContinuousWithinAt Prod.snd s p

theorem ContinuousOn.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β × γ} {s : Set α} (hf : ContinuousOn f s) : ContinuousOn (fun x => (f x).snd) s

theorem ContinuousWithinAt.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β × γ} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) : ContinuousWithinAt (fun x => (f x).snd) s a

theorem continuousWithinAt_prod_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β × γ} {s : Set α} {x : α} : ContinuousWithinAt f s x ↔ ContinuousWithinAt (Prod.fst ∘ f) s x ∧ ContinuousWithinAt (Prod.snd ∘ f) s x