Neighborhoods and continuity relative to a subset

This file defines relative versions

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

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

Notation

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

@[simp]

theorem nhds_bind_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} : ((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_nhdsWithin_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop} : (∀ᶠ (y : α) in nhdsWithin a s, ∀ᶠ (x : α) in nhdsWithin y s, p x) ↔ ∀ᶠ (x : α) in nhdsWithin a s, p x

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

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

theorem nhdsWithin_hasBasis {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {p : β → Prop} {s : β → Set α} {a : α} (h : (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 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_7} {f : ι → α} (h : DenseRange f) (x : α) : (nhdsWithin x (Set.range f)).NeBot

theorem mem_closure_pi {ι : Type u_7} {α : ι → Type u_8} [(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_7} {α : ι → Type u_8} [(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_7} {α : ι → Type u_8} [(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_7} [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

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 ContinuousOn.continuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} (hf : ContinuousOn f s) (hx : x ∈ s) : ContinuousWithinAt f s x

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

theorem 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 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 continuousWithinAt_pi {α : Type u_1} [TopologicalSpace α] {ι : Type u_7} {π : ι → Type u_8} [(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_7} {π : ι → Type u_8} [(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_7} {π : ι → Type u_8} [(i : ι) → TopologicalSpace (π i)] {f : α → (i : ι) → π i} {s : Set α} (hf : ∀ (i : ι), ContinuousOn (fun (y : α) => f y i) s) : ContinuousOn f s

theorem ContinuousWithinAt.fin_insertNth {α : Type u_1} [TopologicalSpace α] {n : ℕ} {π : Fin (n + 1) → Type u_7} [(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_7} [(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 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_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_7} {β : Type u_8} {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_7} {β : Type u_8} {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 ContinuousOn.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {f : α → γ} {g : β → δ} {s : Set α} {t : Set β} (hf : ContinuousOn f s) (hg : ContinuousOn g t) : ContinuousOn (Prod.map f g) (s ×ˢ t)

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

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

@[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 nhdsWithin_le_comap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {x : α} {s : Set α} {f : α → β} (ctsf : ContinuousWithinAt f s x) : nhdsWithin x s ≤ Filter.comap f (nhdsWithin (f x) (f '' s))

@[simp]

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

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

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)

@[simp]

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

@[simp]

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

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

Alias of the reverse direction of continuousWithinAt_insert_self.

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem IsOpenMap.continuousOn_image_of_leftInvOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (h : IsOpenMap (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.congr_mono {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : α → β} {s : Set α} {s₁ : Set α} (h : ContinuousOn f s) (h' : Set.EqOn g f s₁) (h₁ : s₁ ⊆ s) : ContinuousOn g s₁

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Continuous.comp_continuousOn' {α : Type u_7} {β : Type u_8} {γ : Type u_9} [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_apply {ι : Type u_7} {π : ι → Type u_8} [(i : ι) → TopologicalSpace (π i)] (i : ι) (s : Set ((i : ι) → π i)) : ContinuousOn (fun (p : (i : ι) → π i) => p i) 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 Set.LeftInvOn.map_nhdsWithin_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : β → α} {x : β} {s : Set β} (h : Set.LeftInvOn f g s) (hx : f (g x) = x) (hf : ContinuousWithinAt f (g '' s) (g x)) (hg : ContinuousWithinAt g s x) : Filter.map g (nhdsWithin x s) = nhdsWithin (g x) (g '' s)

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

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

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

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

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

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

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

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

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

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

theorem 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_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} {β : Type u_2} [TopologicalSpace α] {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_7} {s : Set α} {T : Set (Set β)} {f : α → β} (h : ∀ t ∈ T, IsOpen (s ∩ f ⁻¹' t)) : ContinuousOn f s

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

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

theorem 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

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

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

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

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

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

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

theorem ContinuousOn.if' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {p : α → Prop} {f : α → β} {g : α → β} [(a : α) → Decidable (p a)] (hpf : ∀ a ∈ 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_7} {β : Type u_8} [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 frontier_inter_open_inter {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} (ht : IsOpen t) : frontier (s ∩ t) ∩ t = frontier s ∩ t

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

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

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