Neighborhoods and continuity relative to a subset

This file develops API on the relative versions

• ContinuousOn of Continuous
• ContinuousWithinAt of ContinuousAt

related to continuity, which are defined in previous definition files. Their basic properties studied in this file include the relationships between these restricted notions and the corresponding notions for the subtype equipped with the subspace topology.

ContinuousWithinAt

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.

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

@[simp]

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

@[deprecated continuousOn_univ (since := "2025-07-04")]

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

Alias of continuousOn_univ.

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 (s.restrict f) ⟨x, h⟩

theorem ContinuousWithinAt.tendsto_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} {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 : α → β} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) : Filter.Tendsto f (nhdsWithin x s) (nhdsWithin (f x) (f '' s))

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

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

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

theorem continuousWithinAt_of_notMem_closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} (hx : x ∉ closure s) : ContinuousWithinAt f s x

@[deprecated continuousWithinAt_of_notMem_closure (since := "2025-05-23")]

theorem continuousWithinAt_of_not_mem_closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} (hx : x ∉ closure s) : ContinuousWithinAt f s x

Alias of continuousWithinAt_of_notMem_closure.

ContinuousOn

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

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 continuousOn_iff_continuous_restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} : ContinuousOn f s ↔ Continuous (s.restrict f)

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

Alias of the forward direction of continuousOn_iff_continuous_restrict.

theorem ContinuousOn.mapsToRestrict {α : 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)

@[deprecated ContinuousOn.mapsToRestrict (since := "05-09-2025")]

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)

Alias of ContinuousOn.mapsToRestrict.

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

theorem ContinuousOn.mono_dom {α : Type u_5} {β : Type u_6} {t₁ 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₂ 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 : Set α), IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s

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

@[simp]

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

@[simp]

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 : s.Subsingleton) (f : α → β) : ContinuousOn f s

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.isOpen_inter_preimage {α : 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_isClosed_of_isClosed {α : 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 ∈ s, ∃ (t : Set α), IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)) : ContinuousOn f s

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

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

Congruence and monotonicity properties with respect to sets

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

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

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

If two sets coincide around x, then being continuous within one or the other at x is equivalent. See also continuousWithinAt_congr_set' which requires that the sets coincide locally away from a point y, in a T1 space.

theorem ContinuousWithinAt.congr_set {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s t : Set α} {x : α} (hf : ContinuousWithinAt f s x) (h : s =ᶠ[nhds x] t) : ContinuousWithinAt f t x

theorem continuousWithinAt_inter' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s 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 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 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 t : Set α} {x : α} (hs : ContinuousWithinAt f s x) (ht : ContinuousWithinAt f t x) : ContinuousWithinAt f (s ∪ t) x

@[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 : α → β} {s : Set α} {x : α} : ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x

theorem ContinuousWithinAt.insert {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} : 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 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

See also continuousWithinAt_diff_singleton for the case of s \ {y}, but requiring `T1Space α.

@[simp]

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

theorem ContinuousOn.mono {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s 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)

Relation between ContinuousAt and ContinuousWithinAt

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 continuousOn_of_forall_continuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (hcont : ∀ x ∈ s, ContinuousAt f x) : ContinuousOn f s

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

Congruence properties with respect to functions

theorem ContinuousOn.congr_mono {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {s 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 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 g : α → β} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) (h₁ : g =ᶠ[nhdsWithin x s] f) (hx : g x = f x) : ContinuousWithinAt g s x

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

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

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

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

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

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

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

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

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

theorem continuousWithinAt_congr_of_insert {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {s : Set α} {x : α} (h₁ : ∀ y ∈ insert x s, g y = f y) : ContinuousWithinAt g s x ↔ ContinuousWithinAt f s x

theorem ContinuousWithinAt.congr_mono {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {s 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 ContinuousAt.congr_of_eventuallyEq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {x : α} (h : ContinuousAt f x) (hg : g =ᶠ[nhds x] f) : ContinuousAt g x

Composition

theorem ContinuousWithinAt.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ} {t : Set β} (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_of_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ} {t : Set β} {y : β} (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x) (h : Set.MapsTo f s t) (hy : f x = y) : ContinuousWithinAt (g ∘ f) s x

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

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

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

theorem ContinuousWithinAt.comp_of_preimage_mem_nhdsWithin_of_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ} {t : Set β} {y : β} (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x) (h : f ⁻¹' t ∈ nhdsWithin x s) (hy : f x = y) : ContinuousWithinAt (g ∘ f) s x

theorem ContinuousWithinAt.comp_of_mem_nhdsWithin_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ} {t : Set β} (hg : ContinuousWithinAt g t (f x)) (hf : ContinuousWithinAt f s x) (hs : t ∈ nhdsWithin (f x) (f '' s)) : ContinuousWithinAt (g ∘ f) s x

theorem ContinuousWithinAt.comp_of_mem_nhdsWithin_image_of_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ} {t : Set β} {y : β} (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x) (hs : t ∈ nhdsWithin y (f '' s)) (hy : f x = y) : ContinuousWithinAt (g ∘ f) s x

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

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

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

See also ContinuousOn.comp' using the form fun y ↦ g (f y) instead of g ∘ 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) (h : Set.MapsTo f s t) : ContinuousOn (fun (x : α) => g (f x)) s

Variant of ContinuousOn.comp using the form fun y ↦ g (f y) instead of g ∘ f.

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

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

See also Continuous.comp_continuousOn' using the form fun y ↦ g (f y) instead of g ∘ f.

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 (fun (x : α) => g (f x)) s

Variant of Continuous.comp_continuousOn using the form fun y ↦ g (f y) instead of g ∘ f.

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 ContinuousOn.image_comp_continuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set α} (hg : ContinuousOn g (f '' s)) (hf : Continuous f) : ContinuousOn (g ∘ f) s

theorem ContinuousAt.comp₂_continuousWithinAt {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {f : β × γ → δ} {g : α → β} {h : α → γ} {x : α} {s : Set α} (hf : ContinuousAt f (g x, h x)) (hg : ContinuousWithinAt g s x) (hh : ContinuousWithinAt h s x) : ContinuousWithinAt (fun (x : α) => f (g x, h x)) s x

theorem ContinuousAt.comp₂_continuousWithinAt_of_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {f : β × γ → δ} {g : α → β} {h : α → γ} {x : α} {s : Set α} {y : β × γ} (hf : ContinuousAt f y) (hg : ContinuousWithinAt g s x) (hh : ContinuousWithinAt h s x) (e : (g x, h x) = y) : ContinuousWithinAt (fun (x : α) => f (g x, h x)) s x

Image

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 : α} {t : Set β} (h : ContinuousWithinAt f s x) (hx : x ∈ closure s) (ht : Set.MapsTo f s t) : f x ∈ closure t

theorem Set.MapsTo.closure_of_continuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {t : Set β} (h : MapsTo f s t) (hc : ∀ x ∈ closure s, ContinuousWithinAt f s x) : 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 : MapsTo f s t) (hc : ContinuousOn f (closure s)) : MapsTo f (closure s) (closure t)

theorem ContinuousWithinAt.image_closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (hf : ∀ 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)

Product

theorem ContinuousWithinAt.prodMk {α : 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.prodMk {α : 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 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).1) 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).1) 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).2) 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).2) 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

theorem ContinuousWithinAt.prodMap {α : 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 ContinuousOn.prodMap {α : 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 continuousWithinAt_prod_of_discrete_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology α] {f : α × β → γ} {s : Set (α × β)} {x : α × β} : ContinuousWithinAt f s x ↔ ContinuousWithinAt (fun (x_1 : β) => f (x.1, x_1)) {b : β | (x.1, b) ∈ s} x.2

theorem continuousWithinAt_prod_of_discrete_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology β] {f : α × β → γ} {s : Set (α × β)} {x : α × β} : ContinuousWithinAt f s x ↔ ContinuousWithinAt (fun (x_1 : α) => f (x_1, x.2)) {a : α | (a, x.2) ∈ s} x.1

theorem continuousAt_prod_of_discrete_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology α] {f : α × β → γ} {x : α × β} : ContinuousAt f x ↔ ContinuousAt (fun (x_1 : β) => f (x.1, x_1)) x.2

theorem continuousAt_prod_of_discrete_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology β] {f : α × β → γ} {x : α × β} : ContinuousAt f x ↔ ContinuousAt (fun (x_1 : α) => f (x_1, x.2)) x.1

theorem continuousOn_prod_of_discrete_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology α] {f : α × β → γ} {s : Set (α × β)} : ContinuousOn f s ↔ ∀ (a : α), ContinuousOn (fun (x : β) => f (a, x)) {b : β | (a, b) ∈ s}

theorem continuousOn_prod_of_discrete_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology β] {f : α × β → γ} {s : Set (α × β)} : ContinuousOn f s ↔ ∀ (b : β), ContinuousOn (fun (x : α) => f (x, b)) {a : α | (a, b) ∈ s}

theorem continuous_prod_of_discrete_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology α] {f : α × β → γ} : Continuous f ↔ ∀ (a : α), Continuous fun (x : β) => f (a, x)

If a function f a b is such that y ↦ f a b is continuous for all a, and a lives in a discrete space, then f is continuous, and vice versa.

theorem continuous_prod_of_discrete_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology β] {f : α × β → γ} : Continuous f ↔ ∀ (b : β), Continuous fun (x : α) => f (x, b)

theorem isOpenMap_prod_of_discrete_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology α] {f : α × β → γ} : IsOpenMap f ↔ ∀ (a : α), IsOpenMap fun (x : β) => f (a, x)

theorem isOpenMap_prod_of_discrete_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology β] {f : α × β → γ} : IsOpenMap f ↔ ∀ (b : β), IsOpenMap fun (x : α) => f (x, b)

theorem ContinuousOn.uncurry_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β → γ} {sα : Set α} {sβ : Set β} (a : α) (ha : a ∈ sα) (h : ContinuousOn (Function.uncurry f) (sα ×ˢ sβ)) : ContinuousOn (f a) sβ

theorem ContinuousOn.uncurry_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β → γ} {sα : Set α} {sβ : Set β} (b : β) (ha : b ∈ sβ) (h : ContinuousOn (Function.uncurry f) (sα ×ˢ sβ)) : ContinuousOn (fun (a : α) => f a b) sα

Pi

theorem continuousWithinAt_pi {α : Type u_1} [TopologicalSpace α] {ι : Type u_5} {X : ι → Type u_6} [(i : ι) → TopologicalSpace (X i)] {f : α → (i : ι) → X 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} {X : ι → Type u_6} [(i : ι) → TopologicalSpace (X i)] {f : α → (i : ι) → X i} {s : Set α} : ContinuousOn f s ↔ ∀ (i : ι), ContinuousOn (fun (y : α) => f y i) s

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

theorem continuousOn_apply {ι : Type u_5} {X : ι → Type u_6} [(i : ι) → TopologicalSpace (X i)] (i : ι) (s : Set ((i : ι) → X i)) : ContinuousOn (fun (p : (i : ι) → X i) => p i) s

Specific functions

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 continuousOn_id' {α : Type u_1} [TopologicalSpace α] (s : Set α) : ContinuousOn (fun (x : α) => x) s

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

theorem ContinuousOn.iterate {α : Type u_1} [TopologicalSpace α] {f : α → α} {s : Set α} (hcont : ContinuousOn f s) (hmaps : Set.MapsTo f s s) (n : ℕ) : ContinuousOn f^[n] s

theorem ContinuousWithinAt.finCons {α : Type u_1} [TopologicalSpace α] {n : ℕ} {X : Fin (n + 1) → Type u_5} [(i : Fin (n + 1)) → TopologicalSpace (X i)] {f : α → X 0} {g : α → (j : Fin n) → X j.succ} {a : α} {s : Set α} (hf : ContinuousWithinAt f s a) (hg : ContinuousWithinAt g s a) : ContinuousWithinAt (fun (a : α) => Fin.cons (f a) (g a)) s a

theorem ContinuousOn.finCons {α : Type u_1} [TopologicalSpace α] {n : ℕ} {X : Fin (n + 1) → Type u_5} [(i : Fin (n + 1)) → TopologicalSpace (X i)] {f : α → X 0} {s : Set α} {g : α → (j : Fin n) → X j.succ} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun (a : α) => Fin.cons (f a) (g a)) s

theorem ContinuousWithinAt.matrixVecCons {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {n : ℕ} {f : α → β} {g : α → Fin n → β} {a : α} {s : Set α} (hf : ContinuousWithinAt f s a) (hg : ContinuousWithinAt g s a) : ContinuousWithinAt (fun (a : α) => Matrix.vecCons (f a) (g a)) s a

theorem ContinuousOn.matrixVecCons {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {n : ℕ} {f : α → β} {g : α → Fin n → β} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun (a : α) => Matrix.vecCons (f a) (g a)) s

theorem ContinuousWithinAt.finSnoc {α : Type u_1} [TopologicalSpace α] {n : ℕ} {X : Fin (n + 1) → Type u_5} [(i : Fin (n + 1)) → TopologicalSpace (X i)] {f : α → (j : Fin n) → X j.castSucc} {g : α → X (Fin.last n)} {a : α} {s : Set α} (hf : ContinuousWithinAt f s a) (hg : ContinuousWithinAt g s a) : ContinuousWithinAt (fun (a : α) => Fin.snoc (f a) (g a)) s a

theorem ContinuousOn.finSnoc {α : Type u_1} [TopologicalSpace α] {n : ℕ} {X : Fin (n + 1) → Type u_5} [(i : Fin (n + 1)) → TopologicalSpace (X i)] {f : α → (j : Fin n) → X j.castSucc} {g : α → X (Fin.last n)} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun (a : α) => Fin.snoc (f a) (g a)) s

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

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

theorem Set.LeftInvOn.map_nhdsWithin_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : β → α} {x : β} {s : Set β} (h : 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 : 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 Topology.IsInducing.continuousWithinAt_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {g : β → γ} (hg : IsInducing g) {s : Set α} {x : α} : ContinuousWithinAt f s x ↔ ContinuousWithinAt (g ∘ f) s x

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

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

theorem Topology.IsInducing.continuousOn_image_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {g : β → γ} {s : Set α} (hf : IsInducing f) : ContinuousOn g (f '' s) ↔ ContinuousOn (g ∘ f) s

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

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

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

theorem Topology.IsQuotientMap.continuousOn_isOpen_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {g : β → γ} (h : IsQuotientMap f) {s : Set β} (hs : IsOpen s) : ContinuousOn g s ↔ ContinuousOn (g ∘ f) (f ⁻¹' s)

theorem IsOpenMap.continuousOn_image_of_leftInvOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (h : IsOpenMap (s.restrict 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.union_continuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s t : Set α} {f : α → β} (s_op : IsOpen s) (hs : ContinuousOn f s) (ht : ∀ x ∈ t, ContinuousAt f x) : ContinuousOn f (s ∪ t)

If f is continuous on an open set s and continuous at each point of another set t then f is continuous on s ∪ t.

theorem ContinuousOn.union_of_isClosed {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s t : Set α} {f : α → β} (hfs : ContinuousOn f s) (hft : ContinuousOn f t) (hs : IsClosed s) (ht : IsClosed t) : ContinuousOn f (s ∪ t)

If a function is continuous on two closed sets, it is also continuous on their union.

theorem continouousOn_union_iff_of_isClosed {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s t : Set α} {f : α → β} (hs : IsClosed s) (ht : IsClosed t) : ContinuousOn f (s ∪ t) ↔ ContinuousOn f s ∧ ContinuousOn f t

A function is continuous on two closed sets iff it is also continuous on their union.

theorem ContinuousOn.union_of_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s t : Set α} {f : α → β} (hfs : ContinuousOn f s) (hft : ContinuousOn f t) (hs : IsOpen s) (ht : IsOpen t) : ContinuousOn f (s ∪ t)

If a function is continuous on two open sets, it is also continuous on their union.

theorem continouousOn_union_iff_of_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s t : Set α} {f : α → β} (hs : IsOpen s) (ht : IsOpen t) : ContinuousOn f (s ∪ t) ↔ ContinuousOn f s ∧ ContinuousOn f t

A function is continuous on two open sets iff it is also continuous on their union.

theorem ContinuousOn.iUnion_of_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {ι : Type u_5} {s : ι → Set α} (hf : ∀ (i : ι), ContinuousOn f (s i)) (hs : ∀ (i : ι), IsOpen (s i)) : ContinuousOn f (⋃ (i : ι), s i)

If a function is continuous on open sets s i, it is continuous on their union

theorem continuousOn_iUnion_iff_of_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {ι : Type u_5} {s : ι → Set α} (hs : ∀ (i : ι), IsOpen (s i)) : ContinuousOn f (⋃ (i : ι), s i) ↔ ∀ (i : ι), ContinuousOn f (s i)

A function is continuous on a union of open sets s i iff it is continuous on each s i.

theorem continuous_of_continuousOn_iUnion_of_isOpen {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {ι : Type u_5} {s : ι → Set α} (hf : ∀ (i : ι), ContinuousOn f (s i)) (hs : ∀ (i : ι), IsOpen (s i)) (hs' : ⋃ (i : ι), s i = Set.univ) : Continuous f

theorem ContinuousOn.tendsto_nhdsSet {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s s' : Set α} {t : Set β} (hf : ContinuousOn f s') (hs' : s' ∈ nhdsSet s) (hst : Set.MapsTo f s t) : Filter.Tendsto f (nhdsSet s) (nhdsSet t)

If f is continuous on some neighbourhood s' of s and f maps s to t, the preimage of a set neighbourhood of t is a set neighbourhood of s.

theorem Continuous.tendsto_nhdsSet {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : α → β} {t : Set β} (hf : Continuous f) (hst : Set.MapsTo f s t) : Filter.Tendsto f (nhdsSet s) (nhdsSet t)

Preimage of a set neighborhood of t under a continuous map f is a set neighborhood of s provided that f maps s to t.

theorem Continuous.tendsto_nhdsSet_nhds {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {b : β} {f : α → β} (h : Continuous f) (h' : Set.EqOn f (fun (x : α) => b) s) : Filter.Tendsto f (nhdsSet s) (nhds b)