# 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} [] {a : α} {s : Set α} :
((nhds a).bind fun (x : α) => ) =
@[simp]
theorem eventually_nhds_nhdsWithin {α : Type u_1} [] {a : α} {s : Set α} {p : αProp} :
(∀ᶠ (y : α) in nhds a, ∀ᶠ (x : α) in , p x) ∀ᶠ (x : α) in , p x
theorem eventually_nhdsWithin_iff {α : Type u_1} [] {a : α} {s : Set α} {p : αProp} :
(∀ᶠ (x : α) in , p x) ∀ᶠ (x : α) in nhds a, x sp x
theorem frequently_nhdsWithin_iff {α : Type u_1} [] {z : α} {s : Set α} {p : αProp} :
(∃ᶠ (x : α) in , p x) ∃ᶠ (x : α) in nhds z, p x x s
theorem mem_closure_ne_iff_frequently_within {α : Type u_1} [] {z : α} {s : Set α} :
z closure (s \ {z}) ∃ᶠ (x : α) in nhdsWithin z {z}, x s
@[simp]
theorem eventually_nhdsWithin_nhdsWithin {α : Type u_1} [] {a : α} {s : Set α} {p : αProp} :
(∀ᶠ (y : α) in , ∀ᶠ (x : α) in , p x) ∀ᶠ (x : α) in , p x
theorem nhdsWithin_eq {α : Type u_1} [] (a : α) (s : Set α) :
= t{t : Set α | a t }, Filter.principal (t s)
theorem nhdsWithin_univ {α : Type u_1} [] (a : α) :
nhdsWithin a Set.univ = nhds a
theorem nhdsWithin_hasBasis {α : Type u_1} {β : Type u_2} [] {p : βProp} {s : βSet α} {a : α} (h : (nhds a).HasBasis p s) (t : Set α) :
().HasBasis p fun (i : β) => s i t
theorem nhdsWithin_basis_open {α : Type u_1} [] (a : α) (t : Set α) :
().HasBasis (fun (u : Set α) => a u ) fun (u : Set α) => u t
theorem mem_nhdsWithin {α : Type u_1} [] {t : Set α} {a : α} {s : Set α} :
t ∃ (u : Set α), a u u s t
theorem mem_nhdsWithin_iff_exists_mem_nhds_inter {α : Type u_1} [] {t : Set α} {a : α} {s : Set α} :
t unhds a, u s t
theorem diff_mem_nhdsWithin_compl {α : Type u_1} [] {x : α} {s : Set α} (hs : s nhds x) (t : Set α) :
s \ t
theorem diff_mem_nhdsWithin_diff {α : Type u_1} [] {x : α} {s : Set α} {t : Set α} (hs : s ) (t' : Set α) :
s \ t' nhdsWithin x (t \ t')
theorem nhds_of_nhdsWithin_of_nhds {α : Type u_1} [] {s : Set α} {t : Set α} {a : α} (h1 : s nhds a) (h2 : t ) :
t nhds a
theorem mem_nhdsWithin_iff_eventually {α : Type u_1} [] {s : Set α} {t : Set α} {x : α} :
t ∀ᶠ (y : α) in nhds x, y sy t
theorem mem_nhdsWithin_iff_eventuallyEq {α : Type u_1} [] {s : Set α} {t : Set α} {x : α} :
t s =ᶠ[nhds x] s t
theorem nhdsWithin_eq_iff_eventuallyEq {α : Type u_1} [] {s : Set α} {t : Set α} {x : α} :
theorem nhdsWithin_le_iff {α : Type u_1} [] {s : Set α} {t : Set α} {x : α} :
t
theorem preimage_nhdsWithin_coinduced' {α : Type u_1} {β : Type u_2} [] {π : αβ} {s : Set β} {t : Set α} {a : α} (h : a t) (hs : s nhds (π a)) :
π ⁻¹' s
theorem mem_nhdsWithin_of_mem_nhds {α : Type u_1} [] {s : Set α} {t : Set α} {a : α} (h : s nhds a) :
s
theorem self_mem_nhdsWithin {α : Type u_1} [] {a : α} {s : Set α} :
s
theorem eventually_mem_nhdsWithin {α : Type u_1} [] {a : α} {s : Set α} :
∀ᶠ (x : α) in , x s
theorem inter_mem_nhdsWithin {α : Type u_1} [] (s : Set α) {t : Set α} {a : α} (h : t nhds a) :
s t
theorem nhdsWithin_mono {α : Type u_1} [] (a : α) {s : Set α} {t : Set α} (h : s t) :
theorem pure_le_nhdsWithin {α : Type u_1} [] {a : α} {s : Set α} (ha : a s) :
theorem mem_of_mem_nhdsWithin {α : Type u_1} [] {a : α} {s : Set α} {t : Set α} (ha : a s) (ht : t ) :
a t
theorem Filter.Eventually.self_of_nhdsWithin {α : Type u_1} [] {p : αProp} {s : Set α} {x : α} (h : ∀ᶠ (y : α) in , p y) (hx : x s) :
p x
theorem tendsto_const_nhdsWithin {α : Type u_1} {β : Type u_2} [] {l : } {s : Set α} {a : α} (ha : a s) :
Filter.Tendsto (fun (x : β) => a) l ()
theorem nhdsWithin_restrict'' {α : Type u_1} [] {a : α} (s : Set α) {t : Set α} (h : t ) :
= nhdsWithin a (s t)
theorem nhdsWithin_restrict' {α : Type u_1} [] {a : α} (s : Set α) {t : Set α} (h : t nhds a) :
= nhdsWithin a (s t)
theorem nhdsWithin_restrict {α : Type u_1} [] {a : α} (s : Set α) {t : Set α} (h₀ : a t) (h₁ : ) :
= nhdsWithin a (s t)
theorem nhdsWithin_le_of_mem {α : Type u_1} [] {a : α} {s : Set α} {t : Set α} (h : s ) :
theorem nhdsWithin_le_nhds {α : Type u_1} [] {a : α} {s : Set α} :
theorem nhdsWithin_eq_nhdsWithin' {α : Type u_1} [] {a : α} {s : Set α} {t : Set α} {u : Set α} (hs : s nhds a) (h₂ : t s = u s) :
=
theorem nhdsWithin_eq_nhdsWithin {α : Type u_1} [] {a : α} {s : Set α} {t : Set α} {u : Set α} (h₀ : a s) (h₁ : ) (h₂ : t s = u s) :
=
@[simp]
theorem nhdsWithin_eq_nhds {α : Type u_1} [] {a : α} {s : Set α} :
= nhds a s nhds a
theorem IsOpen.nhdsWithin_eq {α : Type u_1} [] {a : α} {s : Set α} (h : ) (ha : a s) :
= nhds a
theorem preimage_nhds_within_coinduced {α : Type u_1} {β : Type u_2} [] {π : αβ} {s : Set β} {t : Set α} {a : α} (h : a t) (ht : ) (hs : s nhds (π a)) :
π ⁻¹' s nhds a
@[simp]
theorem nhdsWithin_empty {α : Type u_1} [] (a : α) :
theorem nhdsWithin_union {α : Type u_1} [] (a : α) (s : Set α) (t : Set α) :
nhdsWithin a (s t) =
theorem nhdsWithin_biUnion {α : Type u_1} [] {ι : Type u_5} {I : Set ι} (hI : I.Finite) (s : ιSet α) (a : α) :
nhdsWithin a (iI, s i) = iI, nhdsWithin a (s i)
theorem nhdsWithin_sUnion {α : Type u_1} [] {S : Set (Set α)} (hS : S.Finite) (a : α) :
nhdsWithin a (⋃₀ S) = sS,
theorem nhdsWithin_iUnion {α : Type u_1} [] {ι : Sort u_5} [] (s : ιSet α) (a : α) :
nhdsWithin a (⋃ (i : ι), s i) = ⨆ (i : ι), nhdsWithin a (s i)
theorem nhdsWithin_inter {α : Type u_1} [] (a : α) (s : Set α) (t : Set α) :
nhdsWithin a (s t) =
theorem nhdsWithin_inter' {α : Type u_1} [] (a : α) (s : Set α) (t : Set α) :
nhdsWithin a (s t) =
theorem nhdsWithin_inter_of_mem {α : Type u_1} [] {a : α} {s : Set α} {t : Set α} (h : s ) :
nhdsWithin a (s t) =
theorem nhdsWithin_inter_of_mem' {α : Type u_1} [] {a : α} {s : Set α} {t : Set α} (h : t ) :
nhdsWithin a (s t) =
@[simp]
theorem nhdsWithin_singleton {α : Type u_1} [] (a : α) :
nhdsWithin a {a} = pure a
@[simp]
theorem nhdsWithin_insert {α : Type u_1} [] (a : α) (s : Set α) :
theorem mem_nhdsWithin_insert {α : Type u_1} [] {a : α} {s : Set α} {t : Set α} :
t nhdsWithin a (insert a s) a t t
theorem insert_mem_nhdsWithin_insert {α : Type u_1} [] {a : α} {s : Set α} {t : Set α} (h : t ) :
theorem insert_mem_nhds_iff {α : Type u_1} [] {a : α} {s : Set α} :
@[simp]
theorem nhdsWithin_compl_singleton_sup_pure {α : Type u_1} [] (a : α) :
theorem nhdsWithin_prod {α : Type u_5} [] {β : Type u_6} [] {s : Set α} {u : Set α} {t : Set β} {v : Set β} {a : α} {b : β} (hu : u ) (hv : v ) :
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) = (iI, Filter.comap (fun (x : (i : ι) → α i) => x i) (nhdsWithin (x i) (s i))) ⨅ (i : ι), ⨅ (_ : iI), 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)] (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) = iI, 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 iI, (nhdsWithin (x i) (s i)).NeBot
theorem Filter.Tendsto.piecewise_nhdsWithin {α : Type u_1} {β : Type u_2} [] {f : αβ} {g : αβ} {t : Set α} [(x : α) → Decidable (x t)] {a : α} {s : Set α} {l : } (h₀ : Filter.Tendsto f (nhdsWithin a (s t)) l) (h₁ : Filter.Tendsto g (nhdsWithin a (s t)) l) :
Filter.Tendsto (t.piecewise f g) () l
theorem Filter.Tendsto.if_nhdsWithin {α : Type u_1} {β : Type u_2} [] {f : αβ} {g : αβ} {p : αProp} [] {a : α} {s : Set α} {l : } (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) () l
theorem map_nhdsWithin {α : Type u_1} {β : Type u_2} [] (f : αβ) (a : α) (s : Set α) :
Filter.map f () = t{t : Set α | a t }, Filter.principal (f '' (t s))
theorem tendsto_nhdsWithin_mono_left {α : Type u_1} {β : Type u_2} [] {f : αβ} {a : α} {s : Set α} {t : Set α} {l : } (hst : s t) (h : Filter.Tendsto f () l) :
theorem tendsto_nhdsWithin_mono_right {α : Type u_1} {β : Type u_2} [] {f : βα} {l : } {a : α} {s : Set α} {t : Set α} (hst : s t) (h : Filter.Tendsto f l ()) :
theorem tendsto_nhdsWithin_of_tendsto_nhds {α : Type u_1} {β : Type u_2} [] {f : αβ} {a : α} {s : Set α} {l : } (h : Filter.Tendsto f (nhds a) l) :
theorem eventually_mem_of_tendsto_nhdsWithin {α : Type u_1} {β : Type u_2} [] {f : βα} {a : α} {s : Set α} {l : } (h : Filter.Tendsto f l ()) :
∀ᶠ (i : β) in l, f i s
theorem tendsto_nhds_of_tendsto_nhdsWithin {α : Type u_1} {β : Type u_2} [] {f : βα} {a : α} {s : Set α} {l : } (h : Filter.Tendsto f l ()) :
theorem nhdsWithin_neBot_of_mem {α : Type u_1} [] {s : Set α} {x : α} (hx : x s) :
().NeBot
theorem IsClosed.mem_of_nhdsWithin_neBot {α : Type u_1} [] {s : Set α} (hs : ) {x : α} (hx : ().NeBot) :
x s
theorem DenseRange.nhdsWithin_neBot {α : Type u_1} [] {ι : Type u_5} {f : ια} (h : ) (x : α) :
(nhdsWithin x ()).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) iI, 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 : iI, Dense (s i)) :
Dense (I.pi s)
theorem eventuallyEq_nhdsWithin_iff {α : Type u_1} {β : Type u_2} [] {f : αβ} {g : αβ} {s : Set α} {a : α} :
f =ᶠ[] g ∀ᶠ (x : α) in nhds a, x sf x = g x
theorem eventuallyEq_nhdsWithin_of_eqOn {α : Type u_1} {β : Type u_2} [] {f : αβ} {g : αβ} {s : Set α} {a : α} (h : Set.EqOn f g s) :
f =ᶠ[] g
theorem Set.EqOn.eventuallyEq_nhdsWithin {α : Type u_1} {β : Type u_2} [] {f : αβ} {g : αβ} {s : Set α} {a : α} (h : Set.EqOn f g s) :
f =ᶠ[] g
theorem tendsto_nhdsWithin_congr {α : Type u_1} {β : Type u_2} [] {f : αβ} {g : αβ} {s : Set α} {a : α} {l : } (hfg : xs, f x = g x) (hf : Filter.Tendsto f () l) :
theorem eventually_nhdsWithin_of_forall {α : Type u_1} [] {s : Set α} {a : α} {p : αProp} (h : xs, p x) :
∀ᶠ (x : α) in , p x
theorem tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within {α : Type u_1} {β : Type u_2} [] {a : α} {l : } {s : Set α} (f : βα) (h1 : Filter.Tendsto f l (nhds a)) (h2 : ∀ᶠ (x : β) in l, f x s) :
theorem tendsto_nhdsWithin_iff {α : Type u_1} {β : Type u_2} [] {a : α} {l : } {s : Set α} {f : βα} :
Filter.Tendsto f l () Filter.Tendsto f l (nhds a) ∀ᶠ (n : β) in l, f n s
@[simp]
theorem tendsto_nhdsWithin_range {α : Type u_1} {β : Type u_2} [] {a : α} {l : } {f : βα} :
theorem Filter.EventuallyEq.eq_of_nhdsWithin {α : Type u_1} {β : Type u_2} [] {s : Set α} {f : αβ} {g : αβ} {a : α} (h : f =ᶠ[] g) (hmem : a s) :
f a = g a
theorem eventually_nhdsWithin_of_eventually_nhds {α : Type u_5} [] {s : Set α} {a : α} {p : αProp} (h : ∀ᶠ (x : α) in nhds a, p x) :
∀ᶠ (x : α) in , p x

### nhdsWithin and subtypes #

theorem mem_nhdsWithin_subtype {α : Type u_1} [] {s : Set α} {a : { x : α // x s }} {t : Set { x : α // x s }} {u : Set { x : α // x s }} :
t t Filter.comap Subtype.val (nhdsWithin (a) (Subtype.val '' u))
theorem nhdsWithin_subtype {α : Type u_1} [] (s : Set α) (a : { x : α // x s }) (t : Set { x : α // x s }) :
= Filter.comap Subtype.val (nhdsWithin (a) (Subtype.val '' t))
theorem nhdsWithin_eq_map_subtype_coe {α : Type u_1} [] {s : Set α} {a : α} (h : a s) :
= Filter.map Subtype.val (nhds a, h)
theorem mem_nhds_subtype_iff_nhdsWithin {α : Type u_1} [] {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} [] {s : Set α} {t : Set α} {a : s} :
Subtype.val ⁻¹' t nhds a t nhdsWithin (a) s
theorem eventually_nhds_subtype_iff {α : Type u_1} [] (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} [] (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} [] {s : Set α} {a : α} (h : a s) (f : αβ) (l : ) :
Filter.Tendsto f () l Filter.Tendsto (s.restrict f) (nhds a, h) l
theorem ContinuousWithinAt.tendsto {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {x : α} (h : ) :
Filter.Tendsto f () (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} [] [] {f : αβ} {s : Set α} {x : α} (hf : ) (hx : x s) :
theorem continuousWithinAt_univ {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (x : α) :
ContinuousWithinAt f Set.univ x
theorem continuous_iff_continuousOn_univ {α : Type u_1} {β : Type u_2} [] [] {f : αβ} :
ContinuousOn f Set.univ
theorem continuousWithinAt_iff_continuousAt_restrict {α : Type u_1} {β : Type u_2} [] [] (f : αβ) {x : α} {s : Set α} (h : x s) :
ContinuousAt (s.restrict f) x, h
theorem ContinuousWithinAt.tendsto_nhdsWithin {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {x : α} {s : Set α} {t : Set β} (h : ) (ht : Set.MapsTo f s t) :
Filter.Tendsto f () (nhdsWithin (f x) t)
theorem ContinuousWithinAt.tendsto_nhdsWithin_image {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {x : α} {s : Set α} (h : ) :
Filter.Tendsto f () (nhdsWithin (f x) (f '' s))
theorem ContinuousWithinAt.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] [] [] [] {f : αγ} {g : βδ} {s : Set α} {t : Set β} {x : α} {y : β} (hf : ) (hg : ) :
ContinuousWithinAt (Prod.map f g) (s ×ˢ t) (x, y)
theorem continuousWithinAt_prod_of_discrete_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : α × βγ} {s : Set (α × β)} {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} [] [] [] [] {f : α × βγ} {s : Set (α × β)} {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} [] [] [] [] {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} [] [] [] [] {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} [] [] [] [] {f : α × βγ} {s : Set (α × β)} :
∀ (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} [] [] [] [] {f : α × βγ} {s : Set (α × β)} :
∀ (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} [] [] [] [] {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} [] [] [] [] {f : α × βγ} :
∀ (b : β), Continuous fun (x : α) => f (x, b)
theorem isOpenMap_prod_of_discrete_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : α × βγ} :
∀ (a : α), IsOpenMap fun (x : β) => f (a, x)
theorem isOpenMap_prod_of_discrete_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] [] {f : α × βγ} :
∀ (b : β), IsOpenMap fun (x : α) => f (x, b)
theorem continuousWithinAt_pi {α : Type u_1} [] {ι : Type u_5} {π : ιType u_6} [(i : ι) → TopologicalSpace (π i)] {f : α(i : ι) → π i} {s : Set α} {x : α} :
∀ (i : ι), ContinuousWithinAt (fun (y : α) => f y i) s x
theorem continuousOn_pi {α : Type u_1} [] {ι : Type u_5} {π : ιType u_6} [(i : ι) → TopologicalSpace (π i)] {f : α(i : ι) → π i} {s : Set α} :
∀ (i : ι), ContinuousOn (fun (y : α) => f y i) s
theorem continuousOn_pi' {α : Type u_1} [] {ι : Type u_5} {π : ιType u_6} [(i : ι) → TopologicalSpace (π i)] {f : α(i : ι) → π i} {s : Set α} (hf : ∀ (i : ι), ContinuousOn (fun (y : α) => f y i) s) :
theorem ContinuousWithinAt.fin_insertNth {α : Type u_1} [] {n : } {π : Fin (n + 1)Type u_5} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : απ i} {a : α} {s : Set α} (hf : ) {g : α(j : Fin n) → π (i.succAbove j)} (hg : ) :
ContinuousWithinAt (fun (a : α) => i.insertNth (f a) (g a)) s a
theorem ContinuousOn.fin_insertNth {α : Type u_1} [] {n : } {π : Fin (n + 1)Type u_5} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : απ i} {s : Set α} (hf : ) {g : α(j : Fin n) → π (i.succAbove j)} (hg : ) :
ContinuousOn (fun (a : α) => i.insertNth (f a) (g a)) s
theorem continuousOn_iff {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} :
xs, ∀ (t : Set β), f x t∃ (u : Set α), x u u s f ⁻¹' t
theorem continuousOn_iff_continuous_restrict {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} :
Continuous (s.restrict f)
theorem ContinuousOn.restrict {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} :
Continuous (s.restrict f)

Alias of the forward direction of continuousOn_iff_continuous_restrict.

theorem ContinuousOn.restrict_mapsTo {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {t : Set β} (hf : ) (ht : Set.MapsTo f s t) :
theorem continuousOn_iff' {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} :
∀ (t : Set β), ∃ (u : Set α), f ⁻¹' t s = u s
theorem ContinuousOn.mono_dom {α : Type u_5} {β : Type u_6} {t₁ : } {t₂ : } {t₃ : } (h₁ : t₂ t₁) {s : Set α} {f : αβ} (h₂ : ) :

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₁ : } {t₂ : } {t₃ : } (h₁ : t₂ t₃) {s : Set α} {f : αβ} (h₂ : ) :

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} [] [] {f : αβ} {s : Set α} :
∀ (t : Set β), ∃ (u : Set α), f ⁻¹' t s = u s
theorem ContinuousOn.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] [] [] [] {f : αγ} {g : βδ} {s : Set α} {t : Set β} (hf : ) (hg : ) :
theorem continuous_of_cover_nhds {α : Type u_1} {β : Type u_2} [] [] {ι : Sort u_5} {f : αβ} {s : ιSet α} (hs : ∀ (x : α), ∃ (i : ι), s i nhds x) (hf : ∀ (i : ι), ContinuousOn f (s i)) :
theorem continuousOn_empty {α : Type u_1} {β : Type u_2} [] [] (f : αβ) :
@[simp]
theorem continuousOn_singleton {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (a : α) :
theorem Set.Subsingleton.continuousOn {α : Type u_1} {β : Type u_2} [] [] {s : Set α} (hs : s.Subsingleton) (f : αβ) :
theorem nhdsWithin_le_comap {α : Type u_1} {β : Type u_2} [] [] {x : α} {s : Set α} {f : αβ} (ctsf : ) :
Filter.comap f (nhdsWithin (f x) (f '' s))
@[simp]
theorem comap_nhdsWithin_range {β : Type u_2} [] {α : Type u_5} (f : αβ) (y : β) :
theorem ContinuousWithinAt.mono {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {t : Set α} {x : α} (h : ) (hs : s t) :
theorem ContinuousWithinAt.mono_of_mem {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {t : Set α} {x : α} (h : ) (hs : t ) :
theorem continuousWithinAt_congr_nhds {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {t : Set α} {x : α} (h : = ) :
theorem continuousWithinAt_inter' {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {t : Set α} {x : α} (h : t ) :
theorem continuousWithinAt_inter {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {t : Set α} {x : α} (h : t nhds x) :
theorem continuousWithinAt_union {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {t : Set α} {x : α} :
theorem ContinuousWithinAt.union {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {t : Set α} {x : α} (hs : ) (ht : ) :
theorem ContinuousWithinAt.mem_closure_image {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {x : α} (h : ) (hx : x ) :
f x closure (f '' s)
theorem ContinuousWithinAt.mem_closure {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {x : α} {A : Set β} (h : ) (hx : x ) (hA : Set.MapsTo f s A) :
f x
theorem Set.MapsTo.closure_of_continuousWithinAt {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {t : Set β} (h : Set.MapsTo f s t) (hc : x, ) :
Set.MapsTo f () ()
theorem Set.MapsTo.closure_of_continuousOn {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {t : Set β} (h : Set.MapsTo f s t) (hc : ContinuousOn f ()) :
Set.MapsTo f () ()
theorem ContinuousWithinAt.image_closure {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (hf : x, ) :
f '' closure (f '' s)
theorem ContinuousOn.image_closure {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (hf : ContinuousOn f ()) :
f '' closure (f '' s)
@[simp]
theorem continuousWithinAt_singleton {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {x : α} :
@[simp]
theorem continuousWithinAt_insert_self {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {x : α} {s : Set α} :
theorem ContinuousWithinAt.insert_self {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {x : α} {s : Set α} :
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} [] [] {f : αβ} {s : Set α} {t : Set α} {x : α} (ht : ) :
@[simp]
theorem continuousWithinAt_diff_self {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {x : α} :
ContinuousWithinAt f (s \ {x}) x
@[simp]
theorem continuousWithinAt_compl_self {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {a : α} :
@[simp]
theorem continuousWithinAt_update_same {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} {s : Set α} {x : α} {y : β} :
@[simp]
theorem continuousAt_update_same {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} {x : α} {y : β} :
theorem IsOpenMap.continuousOn_image_of_leftInvOn {α : Type u_1} {β : Type u_2} [] [] {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} [] [] {f : αβ} (hf : ) {finv : βα} (hleft : Function.LeftInverse finv f) :
ContinuousOn finv ()
theorem ContinuousOn.congr_mono {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} {s : Set α} {s₁ : Set α} (h : ) (h' : Set.EqOn g f s₁) (h₁ : s₁ s) :
theorem ContinuousOn.congr {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} {s : Set α} (h : ) (h' : Set.EqOn g f s) :
theorem continuousOn_congr {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} {s : Set α} (h' : Set.EqOn g f s) :
theorem ContinuousAt.continuousWithinAt {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {x : α} (h : ) :
theorem continuousWithinAt_iff_continuousAt {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {x : α} (h : s nhds x) :
theorem ContinuousWithinAt.continuousAt {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {x : α} (h : ) (hs : s nhds x) :
theorem IsOpen.continuousOn_iff {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (hs : ) :
∀ ⦃a : α⦄, a s
theorem ContinuousOn.continuousAt {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {x : α} (h : ) (hx : s nhds x) :
theorem ContinuousAt.continuousOn {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (hcont : xs, ) :
theorem ContinuousWithinAt.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} {s : Set α} {t : Set β} {x : α} (hg : ContinuousWithinAt g t (f x)) (hf : ) (h : Set.MapsTo f s t) :
theorem ContinuousWithinAt.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} {s : Set α} {t : Set β} {x : α} (hg : ContinuousWithinAt g t (f x)) (hf : ) :
theorem ContinuousAt.comp_continuousWithinAt {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} {s : Set α} {x : α} (hg : ContinuousAt g (f x)) (hf : ) :
theorem ContinuousOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} {s : Set α} {t : Set β} (hg : ) (hf : ) (h : Set.MapsTo f s t) :
theorem ContinuousOn.comp'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} {s : Set α} {t : Set β} (hg : ) (hf : ) (h : Set.MapsTo f s t) :
ContinuousOn (fun (x : α) => g (f x)) s
theorem ContinuousOn.mono {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {t : Set α} (hf : ) (h : t s) :
theorem antitone_continuousOn {α : Type u_1} {β : Type u_2} [] [] {f : αβ} :
theorem ContinuousOn.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} {s : Set α} {t : Set β} (hg : ) (hf : ) :
ContinuousOn (g f) (s f ⁻¹' t)
theorem Continuous.continuousOn {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (h : ) :
theorem Continuous.continuousWithinAt {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {x : α} (h : ) :
theorem Continuous.comp_continuousOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} {s : Set α} (hg : ) (hf : ) :
theorem Continuous.comp_continuousOn' {α : Type u_5} {β : Type u_6} {γ : Type u_7} [] [] [] {g : βγ} {f : αβ} {s : Set α} (hg : ) (hf : ) :
ContinuousOn (fun (x : α) => g (f x)) s
theorem ContinuousOn.comp_continuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {g : βγ} {f : αβ} {s : Set β} (hg : ) (hf : ) (hs : ∀ (x : α), f x 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
theorem ContinuousWithinAt.preimage_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {x : α} {s : Set α} {t : Set β} (h : ) (ht : t nhds (f x)) :
f ⁻¹' t
theorem Set.LeftInvOn.map_nhdsWithin_eq {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : βα} {x : β} {s : Set β} (h : ) (hx : f (g x) = x) (hf : ContinuousWithinAt f (g '' s) (g x)) (hg : ) :
Filter.map g () = nhdsWithin (g x) (g '' s)
theorem Function.LeftInverse.map_nhds_eq {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : βα} {x : β} (h : ) (hf : ContinuousWithinAt f () (g x)) (hg : ) :
Filter.map g (nhds x) = nhdsWithin (g x) ()
theorem ContinuousWithinAt.preimage_mem_nhdsWithin' {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {x : α} {s : Set α} {t : Set β} (h : ) (ht : t nhdsWithin (f x) (f '' s)) :
f ⁻¹' t
theorem ContinuousWithinAt.preimage_mem_nhdsWithin'' {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {x : α} {y : β} {s : Set β} {t : Set β} (h : ContinuousWithinAt f (f ⁻¹' s) x) (ht : t ) (hxy : y = f x) :
theorem Filter.EventuallyEq.congr_continuousWithinAt {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} {s : Set α} {x : α} (h : f =ᶠ[] g) (hx : f x = g x) :
theorem ContinuousWithinAt.congr_of_eventuallyEq {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {f₁ : αβ} {s : Set α} {x : α} (h : ) (h₁ : f₁ =ᶠ[] f) (hx : f₁ x = f x) :
theorem ContinuousWithinAt.congr {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {f₁ : αβ} {s : Set α} {x : α} (h : ) (h₁ : ys, f₁ y = f y) (hx : f₁ x = f x) :
theorem ContinuousWithinAt.congr_mono {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {g : αβ} {s : Set α} {s₁ : Set α} {x : α} (h : ) (h' : Set.EqOn g f s₁) (h₁ : s₁ s) (hx : g x = f x) :
theorem continuousOn_const {α : Type u_1} {β : Type u_2} [] [] {s : Set α} {c : β} :
ContinuousOn (fun (x : α) => c) s
theorem continuousWithinAt_const {α : Type u_1} {β : Type u_2} [] [] {b : β} {s : Set α} {x : α} :
ContinuousWithinAt (fun (x : α) => b) s x
theorem continuousOn_id {α : Type u_1} [] {s : Set α} :
theorem continuousOn_id' {α : Type u_1} [] (s : Set α) :
ContinuousOn (fun (x : α) => x) s
theorem continuousWithinAt_id {α : Type u_1} [] {s : Set α} {x : α} :
theorem continuousOn_open_iff {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (hs : ) :
∀ (t : Set β), IsOpen (s f ⁻¹' t)
theorem ContinuousOn.isOpen_inter_preimage {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {t : Set β} (hf : ) (hs : ) (ht : ) :
IsOpen (s f ⁻¹' t)
theorem ContinuousOn.isOpen_preimage {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {t : Set β} (h : ) (hs : ) (hp : f ⁻¹' t s) (ht : ) :
theorem ContinuousOn.preimage_isClosed_of_isClosed {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {t : Set β} (hf : ) (hs : ) (ht : ) :
theorem ContinuousOn.preimage_interior_subset_interior_preimage {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {t : Set β} (hf : ) (hs : ) :
theorem continuousOn_of_locally_continuousOn {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} (h : xs, ∃ (t : Set α), x t ContinuousOn f (s t)) :
theorem continuousOn_to_generateFrom_iff {α : Type u_1} {β : Type u_2} [] {s : Set α} {T : Set (Set β)} {f : αβ} :
xs, tT, f x tf ⁻¹' t
theorem continuousOn_isOpen_of_generateFrom {α : Type u_1} [] {β : Type u_5} {s : Set α} {T : Set (Set β)} {f : αβ} (h : tT, IsOpen (s f ⁻¹' t)) :
theorem ContinuousWithinAt.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : αβ} {g : αγ} {s : Set α} {x : α} (hf : ) (hg : ) :
ContinuousWithinAt (fun (x : α) => (f x, g x)) s x
theorem ContinuousOn.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : αβ} {g : αγ} {s : Set α} (hf : ) (hg : ) :
ContinuousOn (fun (x : α) => (f x, g x)) s
theorem ContinuousAt.comp₂_continuousWithinAt {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [] [] [] [] {f : β × γδ} {g : αβ} {h : αγ} {x : α} {s : Set α} (hf : ContinuousAt f (g x, h x)) (hg : ) (hh : ) :
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} [] [] [] [] {f : β × γδ} {g : αβ} {h : αγ} {x : α} {s : Set α} {y : β × γ} (hf : ) (hg : ) (hh : ) (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} [] [] [] {f : αβ} {g : βγ} (hg : ) {s : Set α} {x : α} :
theorem Inducing.continuousOn_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : αβ} {g : βγ} (hg : ) {s : Set α} :
theorem Embedding.continuousOn_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : αβ} {g : βγ} (hg : ) {s : Set α} :
theorem Embedding.map_nhdsWithin_eq {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (s : Set α) (x : α) :
Filter.map f () = nhdsWithin (f x) (f '' s)
theorem OpenEmbedding.map_nhdsWithin_preimage_eq {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) (s : Set β) (x : α) :
theorem continuousWithinAt_of_not_mem_closure {α : Type u_1} {β : Type u_2} [] [] {f : αβ} {s : Set α} {x : α} (hx : x) :
theorem ContinuousOn.if' {α : Type u_1} {β : Type u_2} [] [] {s : Set α} {p : αProp} {f : αβ} {g : αβ} [(a : α) → Decidable (p a)] (hpf : as frontier {a : α | p a}, Filter.Tendsto f (nhdsWithin a (s {a : α | p a})) (nhds (if p a then f a else g a))) (hpg : as 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} [] [] {s : Set α} {t : Set α} {f : αβ} {g : αβ} [(a : α) → Decidable (a t)] (hpf : as , Filter.Tendsto f (nhdsWithin a (s t)) (nhds (t.piecewise f g a))) (hpg : as , 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} [] [] {p : αProp} [(a : α) → Decidable (p a)] {s : Set α} {f : αβ} {g : αβ} (hp : as 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} [] [] {s : Set α} {t : Set α} {f : αβ} {g : αβ} [(a : α) → Decidable (a t)] (ht : as , f a = g a) (hf : ContinuousOn f (s )) (hg : ContinuousOn g (s )) :
ContinuousOn (t.piecewise f g) s
theorem continuous_if' {α : Type u_1} {β : Type u_2} [] [] {p : αProp} {f : αβ} {g : αβ} [(a : α) → Decidable (p a)] (hpf : afrontier {x : α | p x}, Filter.Tendsto f (nhdsWithin a {x : α | p x}) (nhds (if p a then f a else g a))) (hpg : afrontier {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} [] [] {p : αProp} {f : αβ} {g : αβ} [(a : α) → Decidable (p a)] (hp : afrontier {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} [] [] {p : αProp} {f : αβ} {g : αβ} [(a : α) → Decidable (p a)] (hp : afrontier {x : α | p x}, f a = g a) (hf : ) (hg : ) :
Continuous fun (a : α) => if p a then f a else g a
theorem continuous_if_const {α : Type u_1} {β : Type u_2} [] [] (p : Prop) {f : αβ} {g : αβ} [] (hf : p) (hg : ¬p) :
Continuous fun (a : α) => if p then f a else g a
theorem Continuous.if_const {α : Type u_1} {β : Type u_2} [] [] (p : Prop) {f : αβ} {g : αβ} [] (hf : ) (hg : ) :
Continuous fun (a : α) => if p then f a else g a
theorem continuous_piecewise {α : Type u_1} {β : Type u_2} [] [] {s : Set α} {f : αβ} {g : αβ} [(a : α) → Decidable (a s)] (hs : a, f a = g a) (hf : ContinuousOn f ()) (hg : ContinuousOn g ()) :
Continuous (s.piecewise f g)
theorem Continuous.piecewise {α : Type u_1} {β : Type u_2} [] [] {s : Set α} {f : αβ} {g : αβ} [(a : α) → Decidable (a s)] (hs : a, f a = g a) (hf : ) (hg : ) :
Continuous (s.piecewise f g)
theorem continuous_indicator {α : Type u_1} {β : Type u_2} [] [] [Zero β] {f : αβ} {s : Set α} (hs : a, f a = 0) (hf : ContinuousOn f ()) :
Continuous (s.indicator f)
theorem continuous_mulIndicator {α : Type u_1} {β : Type u_2} [] [] [One β] {f : αβ} {s : Set α} (hs : a, f a = 1) (hf : ContinuousOn f ()) :
Continuous (s.mulIndicator f)
theorem Continuous.indicator {α : Type u_1} {β : Type u_2} [] [] [Zero β] {f : αβ} {s : Set α} (hs : a, f a = 0) (hf : ) :
Continuous (s.indicator f)
theorem Continuous.mulIndicator {α : Type u_1} {β : Type u_2} [] [] [One β] {f : αβ} {s : Set α} (hs : a, f a = 1) (hf : ) :
Continuous (s.mulIndicator f)
theorem IsOpen.ite' {α : Type u_1} [] {s : Set α} {s' : Set α} {t : Set α} (hs : ) (hs' : IsOpen s') (ht : x, x s x s') :
IsOpen (t.ite s s')
theorem IsOpen.ite {α : Type u_1} [] {s : Set α} {s' : Set α} {t : Set α} (hs : ) (hs' : IsOpen s') (ht : s = s' ) :
IsOpen (t.ite s s')
theorem ite_inter_closure_eq_of_inter_frontier_eq {α : Type u_1} [] {s : Set α} {s' : Set α} {t : Set α} (ht : s = s' ) :
t.ite s s' = s
theorem ite_inter_closure_compl_eq_of_inter_frontier_eq {α : Type u_1} [] {s : Set α} {s' : Set α} {t : Set α} (ht : s = s' ) :
t.ite s s' = s'
theorem continuousOn_piecewise_ite' {α : Type u_1} {β : Type u_2} [] [] {s : Set α} {s' : Set α} {t : Set α} {f : αβ} {f' : αβ} [(x : α) → Decidable (x t)] (h : ContinuousOn f (s )) (h' : ContinuousOn f' (s' )) (H : s = s' ) (Heq : Set.EqOn f f' (s )) :
ContinuousOn (t.piecewise f f') (t.ite s s')
theorem continuousOn_piecewise_ite {α : Type u_1} {β : Type u_2} [] [] {s : Set α} {s' : Set α} {t : Set α} {f : αβ} {f' : αβ} [(x : α) → Decidable (x t)] (h : ) (h' : ContinuousOn f' s') (H : s = s' ) (Heq : Set.EqOn f f' (s )) :
ContinuousOn (t.piecewise f f') (t.ite s s')
theorem frontier_inter_open_inter {α : Type u_1} [] {s : Set α} {t : Set α} (ht : ) :
frontier (s t) t = t
theorem continuousOn_fst {α : Type u_1} {β : Type u_2} [] [] {s : Set (α × β)} :
ContinuousOn Prod.fst s
theorem continuousWithinAt_fst {α : Type u_1} {β : Type u_2} [] [] {s : Set (α × β)} {p : α × β} :
ContinuousWithinAt Prod.fst s p
theorem ContinuousOn.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : αβ × γ} {s : Set α} (hf : ) :
ContinuousOn (fun (x : α) => (f x).1) s
theorem ContinuousWithinAt.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : αβ × γ} {s : Set α} {a : α} (h : ) :
ContinuousWithinAt (fun (x : α) => (f x).1) s a
theorem continuousOn_snd {α : Type u_1} {β : Type u_2} [] [] {s : Set (α × β)} :
ContinuousOn Prod.snd s
theorem continuousWithinAt_snd {α : Type u_1} {β : Type u_2} [] [] {s : Set (α × β)} {p : α × β} :
ContinuousWithinAt Prod.snd s p
theorem ContinuousOn.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : αβ × γ} {s : Set α} (hf : ) :
ContinuousOn (fun (x : α) => (f x).2) s
theorem ContinuousWithinAt.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : αβ × γ} {s : Set α} {a : α} (h : ) :
ContinuousWithinAt (fun (x : α) => (f x).2) s a
theorem continuousWithinAt_prod_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] {f : αβ × γ} {s : Set α} {x : α} :
ContinuousWithinAt (Prod.fst f) s x ContinuousWithinAt (Prod.snd f) s x