Neighborhoods and continuity relative to a subset

This file develops API on the relative versions

• nhdsWithin of nhds
• 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.

Notation

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

Properties of the neighborhood-within filter

@[simp]

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

@[simp]

theorem eventually_nhds_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop} : (∀ᶠ (y : α) in nhds a, ∀ᶠ (x : α) in nhdsWithin y s, p x) ↔ ∀ᶠ (x : α) in nhdsWithin a s, p x

theorem eventually_nhdsWithin_iff {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop} : (∀ᶠ (x : α) in nhdsWithin a s, p x) ↔ ∀ᶠ (x : α) in nhds a, x ∈ s → p x

theorem frequently_nhdsWithin_iff {α : Type u_1} [TopologicalSpace α] {z : α} {s : Set α} {p : α → Prop} : (∃ᶠ (x : α) in nhdsWithin z s, p x) ↔ ∃ᶠ (x : α) in nhds z, p x ∧ x ∈ s

theorem mem_closure_ne_iff_frequently_within {α : Type u_1} [TopologicalSpace α] {z : α} {s : Set α} : z ∈ closure (s \ {z}) ↔ ∃ᶠ (x : α) in nhdsWithin z {z}ᶜ, x ∈ s

@[simp]

theorem eventually_eventually_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop} : (∀ᶠ (y : α) in nhdsWithin a s, ∀ᶠ (x : α) in nhdsWithin y s, p x) ↔ ∀ᶠ (x : α) in nhdsWithin a s, p x

@[deprecated eventually_eventually_nhdsWithin]

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

Alias of eventually_eventually_nhdsWithin.

@[simp]

theorem eventually_mem_nhdsWithin_iff {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {t : Set α} : (∀ᶠ (x' : α) in nhdsWithin x s, t ∈ nhdsWithin x' s) ↔ t ∈ nhdsWithin x s

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

@[simp]

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

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

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

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

theorem mem_nhdsWithin_iff_exists_mem_nhds_inter {α : Type u_1} [TopologicalSpace α] {t : Set α} {a : α} {s : Set α} : t ∈ nhdsWithin a s ↔ ∃ u ∈ nhds a, u ∩ s ⊆ t

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

theorem diff_mem_nhdsWithin_diff {α : Type u_1} [TopologicalSpace α] {x : α} {s : 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 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 nhds_eq_nhdsWithin_sup_nhdsWithin {α : Type u_1} [TopologicalSpace α] (b : α) {I₁ : Set α} {I₂ : Set α} (hI : Set.univ = I₁ ∪ I₂) : nhds b = nhdsWithin b I₁ ⊔ nhdsWithin b I₂

theorem union_mem_nhds_of_mem_nhdsWithin {α : Type u_1} [TopologicalSpace α] {b : α} {I₁ : Set α} {I₂ : Set α} (h : Set.univ = I₁ ∪ I₂) {L : Set α} (hL : L ∈ nhdsWithin b I₁) {R : Set α} (hR : R ∈ nhdsWithin b I₂) : L ∪ R ∈ nhds b

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

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

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

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

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

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

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

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

theorem nhdsWithin_inter {α : Type u_1} [TopologicalSpace α] (a : α) (s : 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 : I.Finite) (s : (i : ι) → Set (π i)) (x : (i : ι) → π i) : nhdsWithin x (I.pi s) = ⨅ (i : ι), Filter.comap (fun (x : (i : ι) → π i) => 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 : I.Finite) (s : (i : ι) → Set (π i)) (x : (i : ι) → π i) : nhdsWithin x (I.pi s) = (⨅ i ∈ I, Filter.comap (fun (x : (i : ι) → π i) => x i) (nhdsWithin (x i) (s i))) ⊓ ⨅ (i : ι), ⨅ (_ : i ∉ I), Filter.comap (fun (x : (i : ι) → π i) => x i) (nhds (x i))

theorem nhdsWithin_pi_univ_eq {ι : Type u_5} {π : ι → Type u_6} [(i : ι) → TopologicalSpace (π i)] [Finite ι] (s : (i : ι) → Set (π i)) (x : (i : ι) → π i) : nhdsWithin x (Set.univ.pi s) = ⨅ (i : ι), Filter.comap (fun (x : (i : ι) → π i) => 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 (I.pi s) = ⊥ ↔ ∃ 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} : (nhdsWithin x (I.pi s)).NeBot ↔ ∀ i ∈ I, (nhdsWithin (x i) (s i)).NeBot

instance instNeBotNhdsWithinUnivPi {ι : Type u_5} {π : ι → Type u_6} [(i : ι) → TopologicalSpace (π i)] {s : (i : ι) → Set (π i)} {x : (i : ι) → π i} [∀ (i : ι), (nhdsWithin (x i) (s i)).NeBot] : (nhdsWithin x (Set.univ.pi s)).NeBot

Equations

• ⋯ = ⋯

instance Pi.instNeBotNhdsWithinIio {ι : Type u_5} {π : ι → Type u_6} [(i : ι) → TopologicalSpace (π i)] [Nonempty ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} [∀ (i : ι), (nhdsWithin (x i) (Set.Iio (x i))).NeBot] : (nhdsWithin x (Set.Iio x)).NeBot

Equations

• ⋯ = ⋯

instance Pi.instNeBotNhdsWithinIoi {ι : Type u_5} {π : ι → Type u_6} [(i : ι) → TopologicalSpace (π i)] [Nonempty ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} [∀ (i : ι), (nhdsWithin (x i) (Set.Ioi (x i))).NeBot] : (nhdsWithin x (Set.Ioi x)).NeBot

Equations

• ⋯ = ⋯

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 (t.piecewise f g) (nhdsWithin a s) l

theorem Filter.Tendsto.if_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → β} {g : α → β} {p : α → Prop} [DecidablePred p] {a : α} {s : Set α} {l : Filter β} (h₀ : 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 ∈ {t : Set α | a ∈ t ∧ IsOpen t}, Filter.principal (f '' (t ∩ s))

theorem tendsto_nhdsWithin_mono_left {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → β} {a : α} {s : 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 nhdsWithin_neBot_of_mem {α : Type u_1} [TopologicalSpace α] {s : Set α} {x : α} (hx : x ∈ s) : (nhdsWithin x s).NeBot

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

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

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

theorem closure_pi_set {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → TopologicalSpace (α i)] (I : Set ι) (s : (i : ι) → Set (α i)) : closure (I.pi s) = I.pi fun (i : ι) => closure (s i)

theorem dense_pi {ι : Type u_5} {α : ι → Type u_6} [(i : ι) → TopologicalSpace (α i)] {s : (i : ι) → Set (α i)} (I : Set ι) (hs : ∀ i ∈ I, Dense (s i)) : Dense (I.pi s)

theorem 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 ∈ s, f x = g x) (hf : Filter.Tendsto f (nhdsWithin a s) l) : Filter.Tendsto g (nhdsWithin a s) l

theorem eventually_nhdsWithin_of_forall {α : Type u_1} [TopologicalSpace α] {s : Set α} {a : α} {p : α → Prop} (h : ∀ x ∈ s, p x) : ∀ᶠ (x : α) in nhdsWithin a s, p x

theorem tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {a : α} {l : Filter β} {s : Set α} (f : β → α) (h1 : Filter.Tendsto f l (nhds a)) (h2 : ∀ᶠ (x : β) in l, f x ∈ s) : Filter.Tendsto f l (nhdsWithin a s)

theorem tendsto_nhdsWithin_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {a : α} {l : Filter β} {s : Set α} {f : β → α} : Filter.Tendsto f l (nhdsWithin a s) ↔ Filter.Tendsto f l (nhds a) ∧ ∀ᶠ (n : β) in l, f n ∈ s

@[simp]

theorem tendsto_nhdsWithin_range {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {a : α} {l : Filter β} {f : β → α} : Filter.Tendsto f l (nhdsWithin a (Set.range f)) ↔ Filter.Tendsto f l (nhds a)

theorem Filter.EventuallyEq.eq_of_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {s : Set α} {f : α → β} {g : α → β} {a : α} (h : f =ᶠ[nhdsWithin a s] g) (hmem : a ∈ s) : f a = g a

theorem eventually_nhdsWithin_of_eventually_nhds {α : Type u_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 ⟨a, h⟩)

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

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

theorem eventually_nhds_subtype_iff {α : Type u_1} [TopologicalSpace α] (s : Set α) (a : ↑s) (P : α → Prop) : (∀ᶠ (x : ↑s) in nhds a, P ↑x) ↔ ∀ᶠ (x : α) in nhdsWithin (↑a) s, P x

theorem frequently_nhds_subtype_iff {α : Type u_1} [TopologicalSpace α] (s : Set α) (a : ↑s) (P : α → Prop) : (∃ᶠ (x : ↑s) in nhds a, P ↑x) ↔ ∃ᶠ (x : α) in nhdsWithin (↑a) s, P x

theorem tendsto_nhdsWithin_iff_subtype {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {s : Set α} {a : α} (h : a ∈ s) (f : α → β) (l : Filter β) : Filter.Tendsto f (nhdsWithin a s) l ↔ Filter.Tendsto (s.restrict f) (nhds ⟨a, h⟩) l

Local continuity properties of functions

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

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

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

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.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 : Set α), 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 : Set α), IsClosed u ∧ f ⁻¹' t ∩ s = u ∩ s

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

@[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 α] {β : Type u_5} {s : Set α} {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 : 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 β] {f : α → β} {s : Set α} {t : Set α} {x : α} (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

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

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)

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 ContinuousAt.continuousOn {α : 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 : 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 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 ∈ 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

Composition

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

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.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 Continuous.comp_continuousOn' {α : Type u_5} {β : Type u_6} {γ : Type u_7} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : β → γ} {f : α → β} {s : Set α} (hg : Continuous g) (hf : ContinuousOn f s) : ContinuousOn (fun (x : α) => g (f x)) 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 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 : α} {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 ∈ 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 ∈ 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.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_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.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 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 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

Pi

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

theorem continuousOn_apply {ι : Type u_5} {π : ι → Type u_6} [(i : ι) → TopologicalSpace (π i)] (i : ι) (s : Set ((i : ι) → π i)) : ContinuousOn (fun (p : (i : ι) → π 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.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) → π (i.succAbove j)} (hg : ContinuousWithinAt g s a) : ContinuousWithinAt (fun (a : α) => i.insertNth (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) → π (i.succAbove j)} (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 : 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 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 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

@[deprecated IsOpenEmbedding.map_nhdsWithin_preimage_eq]

theorem OpenEmbedding.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

Alias of IsOpenEmbedding.map_nhdsWithin_preimage_eq.

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

@[deprecated IsQuotientMap.continuousOn_isOpen_iff]

theorem QuotientMap.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)

Alias of IsQuotientMap.continuousOn_isOpen_iff.

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)

Continuity of piecewise defined functions

@[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 ContinuousOn.if' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {p : α → Prop} {f : α → β} {g : α → β} [(a : α) → Decidable (p a)] (hpf : ∀ 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 ∈ 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 ∈ s ∩ frontier t, Filter.Tendsto f (nhdsWithin a (s ∩ t)) (nhds (t.piecewise f g a))) (hpg : ∀ a ∈ s ∩ frontier t, Filter.Tendsto g (nhdsWithin a (s ∩ tᶜ)) (nhds (t.piecewise f g a))) (hf : ContinuousOn f (s ∩ t)) (hg : ContinuousOn g (s ∩ tᶜ)) : ContinuousOn (t.piecewise 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 ∈ 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 ∈ s ∩ frontier t, f a = g a) (hf : ContinuousOn f (s ∩ closure t)) (hg : ContinuousOn g (s ∩ closure tᶜ)) : ContinuousOn (t.piecewise f g) s

theorem continuous_if' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {p : α → Prop} {f : α → β} {g : α → β} [(a : α) → Decidable (p a)] (hpf : ∀ 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 ∈ 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 ∈ 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 ∈ 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 ∈ frontier s, f a = g a) (hf : ContinuousOn f (closure s)) (hg : ContinuousOn g (closure sᶜ)) : Continuous (s.piecewise f g)

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

theorem continuous_indicator {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {f : α → β} {s : Set α} (hs : ∀ a ∈ frontier s, f a = 0) (hf : ContinuousOn f (closure s)) : Continuous (s.indicator f)

theorem continuous_mulIndicator {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [One β] {f : α → β} {s : Set α} (hs : ∀ a ∈ frontier s, f a = 1) (hf : ContinuousOn f (closure s)) : Continuous (s.mulIndicator f)

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

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

theorem IsOpen.ite' {α : Type u_1} [TopologicalSpace α] {s : Set α} {s' : Set α} {t : Set α} (hs : IsOpen s) (hs' : IsOpen s') (ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s') : IsOpen (t.ite 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 (t.ite 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) : t.ite 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) : t.ite 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 (t.piecewise f f') (t.ite 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 (t.piecewise f f') (t.ite s s')

theorem ContinuousOn.union_continuousAt {X : Type u_5} {Y : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set X} {f : X → Y} (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.