mathlib documentation

topology.continuous_on

Neighborhoods and continuity relative to a subset

This file defines relative versions

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

source
def nhds_within {Ξ± : Type u_1} [topological_space Ξ±] :
Ξ± β†’ set Ξ± β†’ filter Ξ±

The "neighborhood within" filter. Elements of 𝓝[s] a are sets containing the intersection of s and a neighborhood of a.

Equations
source
@[simp]
theorem nhds_bind_nhds_within {Ξ± : Type u_1} [topological_space Ξ±] {a : Ξ±} {s : set Ξ±} :
(𝓝 a).bind (Ξ» (x : Ξ±), 𝓝[s] x) = 𝓝[s] a

source
@[simp]
theorem eventually_nhds_nhds_within {Ξ± : Type u_1} [topological_space Ξ±] {a : Ξ±} {s : set Ξ±} {p : Ξ± β†’ Prop} :
(βˆ€αΆ  (y : Ξ±) in 𝓝 a, βˆ€αΆ  (x : Ξ±) in 𝓝[s] y, p x) ↔ βˆ€αΆ  (x : Ξ±) in 𝓝[s] a, p x

source
theorem eventually_nhds_within_iff {Ξ± : Type u_1} [topological_space Ξ±] {a : Ξ±} {s : set Ξ±} {p : Ξ± β†’ Prop} :
(βˆ€αΆ  (x : Ξ±) in 𝓝[s] a, p x) ↔ βˆ€αΆ  (x : Ξ±) in 𝓝 a, x ∈ s β†’ p x

source
@[simp]
theorem eventually_nhds_within_nhds_within {Ξ± : Type u_1} [topological_space Ξ±] {a : Ξ±} {s : set Ξ±} {p : Ξ± β†’ Prop} :
(βˆ€αΆ  (y : Ξ±) in 𝓝[s] a, βˆ€αΆ  (x : Ξ±) in 𝓝[s] y, p x) ↔ βˆ€αΆ  (x : Ξ±) in 𝓝[s] a, p x

source
theorem nhds_within_eq {Ξ± : Type u_1} [topological_space Ξ±] (a : Ξ±) (s : set Ξ±) :
𝓝[s] a = β¨… (t : set Ξ±) (H : t ∈ {t : set Ξ± | a ∈ t ∧ is_open t}), π“Ÿ (t ∩ s)

source
theorem nhds_within_univ {Ξ± : Type u_1} [topological_space Ξ±] (a : Ξ±) :
𝓝[set.univ] a = 𝓝 a

source
theorem nhds_within_has_basis {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] {p : Ξ² β†’ Prop} {s : Ξ² β†’ set Ξ±} {a : Ξ±} (h : (𝓝 a).has_basis p s) (t : set Ξ±) :
(𝓝[t] a).has_basis p (Ξ» (i : Ξ²), s i ∩ t)

source
theorem nhds_within_basis_open {Ξ± : Type u_1} [topological_space Ξ±] (a : Ξ±) (t : set Ξ±) :
(𝓝[t] a).has_basis (Ξ» (u : set Ξ±), a ∈ u ∧ is_open u) (Ξ» (u : set Ξ±), u ∩ t)

source
theorem mem_nhds_within {Ξ± : Type u_1} [topological_space Ξ±] {t : set Ξ±} {a : Ξ±} {s : set Ξ±} :
t ∈ 𝓝[s] a ↔ βˆƒ (u : set Ξ±), is_open u ∧ a ∈ u ∧ u ∩ s βŠ† t

source
theorem mem_nhds_within_iff_exists_mem_nhds_inter {Ξ± : Type u_1} [topological_space Ξ±] {t : set Ξ±} {a : Ξ±} {s : set Ξ±} :
t ∈ 𝓝[s] a ↔ βˆƒ (u : set Ξ±) (H : u ∈ 𝓝 a), u ∩ s βŠ† t

source
theorem diff_mem_nhds_within_compl {X : Type u_1} [topological_space X] {x : X} {s : set X} (hs : s ∈ 𝓝 x) (t : set X) :
s \ t ∈ 𝓝[tᢜ] x

source
theorem nhds_of_nhds_within_of_nhds {Ξ± : Type u_1} [topological_space Ξ±] {s t : set Ξ±} {a : Ξ±} :
s ∈ 𝓝 a β†’ t ∈ 𝓝[s] a β†’ t ∈ 𝓝 a

source
theorem mem_nhds_within_of_mem_nhds {Ξ± : Type u_1} [topological_space Ξ±] {s t : set Ξ±} {a : Ξ±} :
s ∈ 𝓝 a β†’ s ∈ 𝓝[t] a

source
theorem self_mem_nhds_within {Ξ± : Type u_1} [topological_space Ξ±] {a : Ξ±} {s : set Ξ±} :
s ∈ 𝓝[s] a

source
theorem inter_mem_nhds_within {Ξ± : Type u_1} [topological_space Ξ±] (s : set Ξ±) {t : set Ξ±} {a : Ξ±} :
t ∈ 𝓝 a β†’ s ∩ t ∈ 𝓝[s] a

source
theorem nhds_within_mono {Ξ± : Type u_1} [topological_space Ξ±] (a : Ξ±) {s t : set Ξ±} :
s βŠ† t β†’ 𝓝[s] a ≀ 𝓝[t] a

source
theorem pure_le_nhds_within {Ξ± : Type u_1} [topological_space Ξ±] {a : Ξ±} {s : set Ξ±} :
a ∈ s β†’ pure a ≀ 𝓝[s] a

source
theorem mem_of_mem_nhds_within {Ξ± : Type u_1} [topological_space Ξ±] {a : Ξ±} {s t : set Ξ±} :
a ∈ s β†’ t ∈ 𝓝[s] a β†’ a ∈ t

source
theorem filter.eventually.self_of_nhds_within {Ξ± : Type u_1} [topological_space Ξ±] {p : Ξ± β†’ Prop} {s : set Ξ±} {x : Ξ±} :
(βˆ€αΆ  (y : Ξ±) in 𝓝[s] x, p y) β†’ x ∈ s β†’ p x

source
theorem tendsto_const_nhds_within {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] {l : filter Ξ²} {s : set Ξ±} {a : Ξ±} :
a ∈ s β†’ filter.tendsto (Ξ» (x : Ξ²), a) l (𝓝[s] a)

source
theorem nhds_within_restrict'' {Ξ± : Type u_1} [topological_space Ξ±] {a : Ξ±} (s : set Ξ±) {t : set Ξ±} :
t ∈ 𝓝[s] a β†’ 𝓝[s] a = 𝓝[s ∩ t] a

source
theorem nhds_within_restrict' {Ξ± : Type u_1} [topological_space Ξ±] {a : Ξ±} (s : set Ξ±) {t : set Ξ±} :
t ∈ 𝓝 a β†’ 𝓝[s] a = 𝓝[s ∩ t] a

source
theorem nhds_within_restrict {Ξ± : Type u_1} [topological_space Ξ±] {a : Ξ±} (s : set Ξ±) {t : set Ξ±} :
a ∈ t β†’ is_open t β†’ 𝓝[s] a = 𝓝[s ∩ t] a

source
theorem nhds_within_le_of_mem {Ξ± : Type u_1} [topological_space Ξ±] {a : Ξ±} {s t : set Ξ±} :
s ∈ 𝓝[t] a β†’ 𝓝[t] a ≀ 𝓝[s] a

source
theorem nhds_within_eq_nhds_within {Ξ± : Type u_1} [topological_space Ξ±] {a : Ξ±} {s t u : set Ξ±} :
a ∈ s β†’ is_open s β†’ t ∩ s = u ∩ s β†’ 𝓝[t] a = 𝓝[u] a

source
theorem nhds_within_eq_of_open {Ξ± : Type u_1} [topological_space Ξ±] {a : Ξ±} {s : set Ξ±} :
a ∈ s β†’ is_open s β†’ 𝓝[s] a = 𝓝 a

source
@[simp]
theorem nhds_within_empty {Ξ± : Type u_1} [topological_space Ξ±] (a : Ξ±) :
𝓝[βˆ…] a = βŠ₯

source
theorem nhds_within_union {Ξ± : Type u_1} [topological_space Ξ±] (a : Ξ±) (s t : set Ξ±) :
𝓝[s βˆͺ t] a = 𝓝[s] a βŠ” 𝓝[t] a

source
theorem nhds_within_inter {Ξ± : Type u_1} [topological_space Ξ±] (a : Ξ±) (s t : set Ξ±) :
𝓝[s ∩ t] a = 𝓝[s] a βŠ“ 𝓝[t] a

source
theorem nhds_within_inter' {Ξ± : Type u_1} [topological_space Ξ±] (a : Ξ±) (s t : set Ξ±) :
𝓝[s ∩ t] a = 𝓝[s] a βŠ“ π“Ÿ t

source
theorem mem_nhds_within_insert {Ξ± : Type u_1} [topological_space Ξ±] {a : Ξ±} {s t : set Ξ±} :
t ∈ 𝓝[s] a β†’ insert a t ∈ 𝓝[insert a s] a

source
theorem nhds_within_prod_eq {Ξ± : Type u_1} [topological_space Ξ±] {Ξ² : Type u_2} [topological_space Ξ²] (a : Ξ±) (b : Ξ²) (s : set Ξ±) (t : set Ξ²) :
𝓝[s.prod t] (a, b) = 𝓝[s] a Γ—αΆ  𝓝[t] b

source
theorem nhds_within_prod {Ξ± : Type u_1} [topological_space Ξ±] {Ξ² : Type u_2} [topological_space Ξ²] {s u : set Ξ±} {t v : set Ξ²} {a : Ξ±} {b : Ξ²} :
u ∈ 𝓝[s] a β†’ v ∈ 𝓝[t] b β†’ u.prod v ∈ 𝓝[s.prod t] (a, b)

source
theorem tendsto_if_nhds_within {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] {f g : Ξ± β†’ Ξ²} {p : Ξ± β†’ Prop} [decidable_pred p] {a : Ξ±} {s : set Ξ±} {l : filter Ξ²} :
filter.tendsto f (𝓝[s ∩ p] a) l β†’ filter.tendsto g (𝓝[s ∩ {x : Ξ± | Β¬p x}] a) l β†’ filter.tendsto (Ξ» (x : Ξ±), ite (p x) (f x) (g x)) (𝓝[s] a) l

source
theorem map_nhds_within {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] (f : Ξ± β†’ Ξ²) (a : Ξ±) (s : set Ξ±) :
filter.map f (𝓝[s] a) = β¨… (t : set Ξ±) (H : t ∈ {t : set Ξ± | a ∈ t ∧ is_open t}), π“Ÿ (f '' (t ∩ s))

source
theorem tendsto_nhds_within_mono_left {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] {f : Ξ± β†’ Ξ²} {a : Ξ±} {s t : set Ξ±} {l : filter Ξ²} :
s βŠ† t β†’ filter.tendsto f (𝓝[t] a) l β†’ filter.tendsto f (𝓝[s] a) l

source
theorem tendsto_nhds_within_mono_right {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] {f : Ξ² β†’ Ξ±} {l : filter Ξ²} {a : Ξ±} {s t : set Ξ±} :
s βŠ† t β†’ filter.tendsto f l (𝓝[s] a) β†’ filter.tendsto f l (𝓝[t] a)

source
theorem tendsto_nhds_within_of_tendsto_nhds {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] {f : Ξ± β†’ Ξ²} {a : Ξ±} {s : set Ξ±} {l : filter Ξ²} :
filter.tendsto f (𝓝 a) l β†’ filter.tendsto f (𝓝[s] a) l

source
theorem principal_subtype {Ξ± : Type u_1} (s : set Ξ±) (t : set {x // x ∈ s}) :
π“Ÿ t = filter.comap coe (π“Ÿ (coe '' t))

source
theorem mem_closure_iff_nhds_within_ne_bot {Ξ± : Type u_1} [topological_space Ξ±] {s : set Ξ±} {x : Ξ±} :
x ∈ closure s ↔ (𝓝[s] x).ne_bot

source
theorem nhds_within_ne_bot_of_mem {Ξ± : Type u_1} [topological_space Ξ±] {s : set Ξ±} {x : Ξ±} :
x ∈ s β†’ (𝓝[s] x).ne_bot

source
theorem is_closed.mem_of_nhds_within_ne_bot {Ξ± : Type u_1} [topological_space Ξ±] {s : set Ξ±} (hs : is_closed s) {x : Ξ±} :
(𝓝[s] x).ne_bot β†’ x ∈ s

source
theorem dense_range.nhds_within_ne_bot {Ξ± : Type u_1} [topological_space Ξ±] {ΞΉ : Type u_2} {f : ΞΉ β†’ Ξ±} (h : dense_range f) (x : Ξ±) :
(𝓝[set.range f] x).ne_bot

source
theorem eventually_eq_nhds_within_iff {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] {f g : Ξ± β†’ Ξ²} {s : set Ξ±} {a : Ξ±} :
f =αΆ [𝓝[s] a] g ↔ βˆ€αΆ  (x : Ξ±) in 𝓝 a, x ∈ s β†’ f x = g x

source
theorem eventually_eq_nhds_within_of_eq_on {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] {f g : Ξ± β†’ Ξ²} {s : set Ξ±} {a : Ξ±} :
set.eq_on f g s β†’ f =αΆ [𝓝[s] a] g

source
theorem set.eq_on.eventually_eq_nhds_within {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] {f g : Ξ± β†’ Ξ²} {s : set Ξ±} {a : Ξ±} :
set.eq_on f g s β†’ f =αΆ [𝓝[s] a] g

source
theorem tendsto_nhds_within_congr {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] {f g : Ξ± β†’ Ξ²} {s : set Ξ±} {a : Ξ±} {l : filter Ξ²} :
(βˆ€ (x : Ξ±), x ∈ s β†’ f x = g x) β†’ filter.tendsto f (𝓝[s] a) l β†’ filter.tendsto g (𝓝[s] a) l

source
theorem eventually_nhds_with_of_forall {Ξ± : Type u_1} [topological_space Ξ±] {s : set Ξ±} {a : Ξ±} {p : Ξ± β†’ Prop} :
(βˆ€ (x : Ξ±), x ∈ s β†’ p x) β†’ (βˆ€αΆ  (x : Ξ±) in 𝓝[s] a, p x)

source
theorem tendsto_nhds_within_of_tendsto_nhds_of_eventually_within {Ξ± : Type u_1} [topological_space Ξ±] {Ξ² : Type u_2} {a : Ξ±} {l : filter Ξ²} {s : set Ξ±} (f : Ξ² β†’ Ξ±) :
filter.tendsto f l (𝓝 a) β†’ (βˆ€αΆ  (x : Ξ²) in l, f x ∈ s) β†’ filter.tendsto f l (𝓝[s] a)

source
theorem filter.eventually_eq.eq_of_nhds_within {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] {s : set Ξ±} {f g : Ξ± β†’ Ξ²} {a : Ξ±} :
f =αΆ [𝓝[s] a] g β†’ a ∈ s β†’ f a = g a

source
theorem eventually_nhds_within_of_eventually_nhds {Ξ± : Type u_1} [topological_space Ξ±] {s : set Ξ±} {a : Ξ±} {p : Ξ± β†’ Prop} :
(βˆ€αΆ  (x : Ξ±) in 𝓝 a, p x) β†’ (βˆ€αΆ  (x : Ξ±) in 𝓝[s] a, p x)

nhds_within and subtypes

source
theorem mem_nhds_within_subtype {Ξ± : Type u_1} [topological_space Ξ±] {s : set Ξ±} {a : {x // x ∈ s}} {t u : set {x // x ∈ s}} :
t ∈ 𝓝[u] a ↔ t ∈ filter.comap coe (𝓝[coe '' u] ↑a)

source
theorem nhds_within_subtype {Ξ± : Type u_1} [topological_space Ξ±] (s : set Ξ±) (a : {x // x ∈ s}) (t : set {x // x ∈ s}) :
𝓝[t] a = filter.comap coe (𝓝[coe '' t] ↑a)

source
theorem nhds_within_eq_map_subtype_coe {Ξ± : Type u_1} [topological_space Ξ±] {s : set Ξ±} {a : Ξ±} (h : a ∈ s) :
𝓝[s] a = filter.map coe (𝓝 ⟨a, h⟩)

source
theorem tendsto_nhds_within_iff_subtype {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] {s : set Ξ±} {a : Ξ±} (h : a ∈ s) (f : Ξ± β†’ Ξ²) (l : filter Ξ²) :
filter.tendsto f (𝓝[s] a) l ↔ filter.tendsto (set.restrict f s) (𝓝 ⟨a, h⟩) l

source
def continuous_within_at {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] :
(Ξ± β†’ Ξ²) β†’ set Ξ± β†’ Ξ± β†’ Prop

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

Equations
source
theorem continuous_within_at.tendsto {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} {x : Ξ±} :
continuous_within_at f s x β†’ filter.tendsto f (𝓝[s] x) (𝓝 (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 tendsto.comp as continuous_within_at.comp will have a different meaning.

source
def continuous_on {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] :
(Ξ± β†’ Ξ²) β†’ set Ξ± β†’ Prop

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

Equations
source
theorem continuous_on.continuous_within_at {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} {x : Ξ±} :
continuous_on f s β†’ x ∈ s β†’ continuous_within_at f s x

source
theorem continuous_within_at_univ {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] (f : Ξ± β†’ Ξ²) (x : Ξ±) :
continuous_within_at f set.univ x ↔ continuous_at f x

source
theorem continuous_within_at_iff_continuous_at_restrict {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] (f : Ξ± β†’ Ξ²) {x : Ξ±} {s : set Ξ±} (h : x ∈ s) :
continuous_within_at f s x ↔ continuous_at (set.restrict f s) ⟨x, h⟩

source
theorem continuous_within_at.tendsto_nhds_within_image {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {x : Ξ±} {s : set Ξ±} :
continuous_within_at f s x β†’ filter.tendsto f (𝓝[s] x) (𝓝[f '' s] f x)

source
theorem continuous_within_at.prod_map {Ξ± : Type u_1} {Ξ² : Type u_2} {Ξ³ : Type u_3} {Ξ΄ : Type u_4} [topological_space Ξ±] [topological_space Ξ²] [topological_space Ξ³] [topological_space Ξ΄] {f : Ξ± β†’ Ξ³} {g : Ξ² β†’ Ξ΄} {s : set Ξ±} {t : set Ξ²} {x : Ξ±} {y : Ξ²} :
continuous_within_at f s x β†’ continuous_within_at g t y β†’ continuous_within_at (prod.map f g) (s.prod t) (x, y)

source
theorem continuous_on_iff {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} :
continuous_on f s ↔ βˆ€ (x : Ξ±), x ∈ s β†’ βˆ€ (t : set Ξ²), is_open t β†’ f x ∈ t β†’ (βˆƒ (u : set Ξ±), is_open u ∧ x ∈ u ∧ u ∩ s βŠ† f ⁻¹' t)

source
theorem continuous_on_iff_continuous_restrict {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} :
continuous_on f s ↔ continuous (set.restrict f s)

source
theorem continuous_on_iff' {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} :
continuous_on f s ↔ βˆ€ (t : set Ξ²), is_open t β†’ (βˆƒ (u : set Ξ±), is_open u ∧ f ⁻¹' t ∩ s = u ∩ s)

source
theorem continuous_on_iff_is_closed {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} :
continuous_on f s ↔ βˆ€ (t : set Ξ²), is_closed t β†’ (βˆƒ (u : set Ξ±), is_closed u ∧ f ⁻¹' t ∩ s = u ∩ s)

source
theorem continuous_on.prod_map {Ξ± : Type u_1} {Ξ² : Type u_2} {Ξ³ : Type u_3} {Ξ΄ : Type u_4} [topological_space Ξ±] [topological_space Ξ²] [topological_space Ξ³] [topological_space Ξ΄] {f : Ξ± β†’ Ξ³} {g : Ξ² β†’ Ξ΄} {s : set Ξ±} {t : set Ξ²} :
continuous_on f s β†’ continuous_on g t β†’ continuous_on (prod.map f g) (s.prod t)

source
theorem continuous_on_empty {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] (f : Ξ± β†’ Ξ²) :
continuous_on f βˆ…

source
theorem nhds_within_le_comap {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {x : Ξ±} {s : set Ξ±} {f : Ξ± β†’ Ξ²} :
continuous_within_at f s x β†’ 𝓝[s] x ≀ filter.comap f (𝓝[f '' s] f x)

source
theorem continuous_within_at_iff_ptendsto_res {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] (f : Ξ± β†’ Ξ²) {x : Ξ±} {s : set Ξ±} :
continuous_within_at f s x ↔ filter.ptendsto (pfun.res f s) (𝓝 x) (𝓝 (f x))

source
theorem continuous_iff_continuous_on_univ {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} :
continuous f ↔ continuous_on f set.univ

source
theorem continuous_within_at.mono {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s t : set Ξ±} {x : Ξ±} :
continuous_within_at f t x β†’ s βŠ† t β†’ continuous_within_at f s x

source
theorem continuous_within_at_inter' {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s t : set Ξ±} {x : Ξ±} :
t ∈ 𝓝[s] x β†’ (continuous_within_at f (s ∩ t) x ↔ continuous_within_at f s x)

source
theorem continuous_within_at_inter {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s t : set Ξ±} {x : Ξ±} :
t ∈ 𝓝 x β†’ (continuous_within_at f (s ∩ t) x ↔ continuous_within_at f s x)

source
theorem continuous_within_at.union {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s t : set Ξ±} {x : Ξ±} :
continuous_within_at f s x β†’ continuous_within_at f t x β†’ continuous_within_at f (s βˆͺ t) x

source
theorem continuous_within_at.mem_closure_image {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} {x : Ξ±} :
continuous_within_at f s x β†’ x ∈ closure s β†’ f x ∈ closure (f '' s)

source
theorem continuous_within_at.mem_closure {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} {x : Ξ±} {A : set Ξ²} :
continuous_within_at f s x β†’ x ∈ closure s β†’ s βŠ† f ⁻¹' A β†’ f x ∈ closure A

source
theorem continuous_within_at.image_closure {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} :
(βˆ€ (x : Ξ±), x ∈ closure s β†’ continuous_within_at f s x) β†’ f '' closure s βŠ† closure (f '' s)

source
theorem continuous_within_at_singleton {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {x : Ξ±} :
continuous_within_at f {x} x

source
theorem continuous_within_at.diff_iff {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s t : set Ξ±} {x : Ξ±} :
continuous_within_at f t x β†’ (continuous_within_at f (s \ t) x ↔ continuous_within_at f s x)

source
@[simp]
theorem continuous_within_at_diff_self {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} {x : Ξ±} :
continuous_within_at f (s \ {x}) x ↔ continuous_within_at f s x

source
theorem is_open_map.continuous_on_image_of_left_inv_on {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} (h : is_open_map (set.restrict f s)) {finv : Ξ² β†’ Ξ±} :
set.left_inv_on finv f s β†’ continuous_on finv (f '' s)

source
theorem is_open_map.continuous_on_range_of_left_inverse {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} (hf : is_open_map f) {finv : Ξ² β†’ Ξ±} :
function.left_inverse finv f β†’ continuous_on finv (set.range f)

source
theorem continuous_on.congr_mono {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f g : Ξ± β†’ Ξ²} {s s₁ : set Ξ±} :
continuous_on f s β†’ set.eq_on g f s₁ β†’ s₁ βŠ† s β†’ continuous_on g s₁

source
theorem continuous_on.congr {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f g : Ξ± β†’ Ξ²} {s : set Ξ±} :
continuous_on f s β†’ set.eq_on g f s β†’ continuous_on g s

source
theorem continuous_on_congr {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f g : Ξ± β†’ Ξ²} {s : set Ξ±} :
set.eq_on g f s β†’ (continuous_on g s ↔ continuous_on f s)

source
theorem continuous_at.continuous_within_at {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} {x : Ξ±} :
continuous_at f x β†’ continuous_within_at f s x

source
theorem continuous_within_at.continuous_at {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} {x : Ξ±} :
continuous_within_at f s x β†’ s ∈ 𝓝 x β†’ continuous_at f x

source
theorem continuous_on.continuous_at {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} {x : Ξ±} :
continuous_on f s β†’ s ∈ 𝓝 x β†’ continuous_at f x

source
theorem continuous_within_at.comp {Ξ± : Type u_1} {Ξ² : Type u_2} {Ξ³ : Type u_3} [topological_space Ξ±] [topological_space Ξ²] [topological_space Ξ³] {g : Ξ² β†’ Ξ³} {f : Ξ± β†’ Ξ²} {s : set Ξ±} {t : set Ξ²} {x : Ξ±} :
continuous_within_at g t (f x) β†’ continuous_within_at f s x β†’ s βŠ† f ⁻¹' t β†’ continuous_within_at (g ∘ f) s x

source
theorem continuous_within_at.comp' {Ξ± : Type u_1} {Ξ² : Type u_2} {Ξ³ : Type u_3} [topological_space Ξ±] [topological_space Ξ²] [topological_space Ξ³] {g : Ξ² β†’ Ξ³} {f : Ξ± β†’ Ξ²} {s : set Ξ±} {t : set Ξ²} {x : Ξ±} :
continuous_within_at g t (f x) β†’ continuous_within_at f s x β†’ continuous_within_at (g ∘ f) (s ∩ f ⁻¹' t) x

source
theorem continuous_on.comp {Ξ± : Type u_1} {Ξ² : Type u_2} {Ξ³ : Type u_3} [topological_space Ξ±] [topological_space Ξ²] [topological_space Ξ³] {g : Ξ² β†’ Ξ³} {f : Ξ± β†’ Ξ²} {s : set Ξ±} {t : set Ξ²} :
continuous_on g t β†’ continuous_on f s β†’ s βŠ† f ⁻¹' t β†’ continuous_on (g ∘ f) s

source
theorem continuous_on.mono {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s t : set Ξ±} :
continuous_on f s β†’ t βŠ† s β†’ continuous_on f t

source
theorem continuous_on.comp' {Ξ± : Type u_1} {Ξ² : Type u_2} {Ξ³ : Type u_3} [topological_space Ξ±] [topological_space Ξ²] [topological_space Ξ³] {g : Ξ² β†’ Ξ³} {f : Ξ± β†’ Ξ²} {s : set Ξ±} {t : set Ξ²} :
continuous_on g t β†’ continuous_on f s β†’ continuous_on (g ∘ f) (s ∩ f ⁻¹' t)

source
theorem continuous.continuous_on {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} :
continuous f β†’ continuous_on f s

source
theorem continuous.continuous_within_at {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} {x : Ξ±} :
continuous f β†’ continuous_within_at f s x

source
theorem continuous.comp_continuous_on {Ξ± : Type u_1} {Ξ² : Type u_2} {Ξ³ : Type u_3} [topological_space Ξ±] [topological_space Ξ²] [topological_space Ξ³] {g : Ξ² β†’ Ξ³} {f : Ξ± β†’ Ξ²} {s : set Ξ±} :
continuous g β†’ continuous_on f s β†’ continuous_on (g ∘ f) s

source
theorem continuous_on.comp_continuous {Ξ± : Type u_1} {Ξ² : Type u_2} {Ξ³ : Type u_3} [topological_space Ξ±] [topological_space Ξ²] [topological_space Ξ³] {g : Ξ² β†’ Ξ³} {f : Ξ± β†’ Ξ²} {s : set Ξ²} :
continuous_on g s β†’ continuous f β†’ set.range f βŠ† s β†’ continuous (g ∘ f)

source
theorem continuous_within_at.preimage_mem_nhds_within {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {x : Ξ±} {s : set Ξ±} {t : set Ξ²} :
continuous_within_at f s x β†’ t ∈ 𝓝 (f x) β†’ f ⁻¹' t ∈ 𝓝[s] x

source
theorem continuous_within_at.preimage_mem_nhds_within' {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {x : Ξ±} {s : set Ξ±} {t : set Ξ²} :
continuous_within_at f s x β†’ t ∈ 𝓝[f '' s] f x β†’ f ⁻¹' t ∈ 𝓝[s] x

source
theorem continuous_within_at.congr_of_eventually_eq {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f f₁ : Ξ± β†’ Ξ²} {s : set Ξ±} {x : Ξ±} :
continuous_within_at f s x β†’ f₁ =αΆ [𝓝[s] x] f β†’ f₁ x = f x β†’ continuous_within_at f₁ s x

source
theorem continuous_within_at.congr {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f f₁ : Ξ± β†’ Ξ²} {s : set Ξ±} {x : Ξ±} :
continuous_within_at f s x β†’ (βˆ€ (y : Ξ±), y ∈ s β†’ f₁ y = f y) β†’ f₁ x = f x β†’ continuous_within_at f₁ s x

source
theorem continuous_within_at.congr_mono {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f g : Ξ± β†’ Ξ²} {s s₁ : set Ξ±} {x : Ξ±} :
continuous_within_at f s x β†’ set.eq_on g f s₁ β†’ s₁ βŠ† s β†’ g x = f x β†’ continuous_within_at g s₁ x

source
theorem continuous_on_const {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {s : set Ξ±} {c : Ξ²} :
continuous_on (Ξ» (x : Ξ±), c) s

source
theorem continuous_within_at_const {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {b : Ξ²} {s : set Ξ±} {x : Ξ±} :
continuous_within_at (Ξ» (_x : Ξ±), b) s x

source
theorem continuous_on_id {Ξ± : Type u_1} [topological_space Ξ±] {s : set Ξ±} :
continuous_on id s

source
theorem continuous_within_at_id {Ξ± : Type u_1} [topological_space Ξ±] {s : set Ξ±} {x : Ξ±} :
continuous_within_at id s x

source
theorem continuous_on_open_iff {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} :
is_open s β†’ (continuous_on f s ↔ βˆ€ (t : set Ξ²), is_open t β†’ is_open (s ∩ f ⁻¹' t))

source
theorem continuous_on.preimage_open_of_open {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} {t : set Ξ²} :
continuous_on f s β†’ is_open s β†’ is_open t β†’ is_open (s ∩ f ⁻¹' t)

source
theorem continuous_on.preimage_closed_of_closed {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} {t : set Ξ²} :
continuous_on f s β†’ is_closed s β†’ is_closed t β†’ is_closed (s ∩ f ⁻¹' t)

source
theorem continuous_on.preimage_interior_subset_interior_preimage {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} {t : set Ξ²} :
continuous_on f s β†’ is_open s β†’ s ∩ f ⁻¹' interior t βŠ† s ∩ interior (f ⁻¹' t)

source
theorem continuous_on_of_locally_continuous_on {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} :
(βˆ€ (x : Ξ±), x ∈ s β†’ (βˆƒ (t : set Ξ±), is_open t ∧ x ∈ t ∧ continuous_on f (s ∩ t))) β†’ continuous_on f s

source
theorem continuous_on_open_of_generate_from {Ξ± : Type u_1} [topological_space Ξ±] {Ξ² : Type u_2} {s : set Ξ±} {T : set (set Ξ²)} {f : Ξ± β†’ Ξ²} :
is_open s β†’ (βˆ€ (t : set Ξ²), t ∈ T β†’ is_open (s ∩ f ⁻¹' t)) β†’ continuous_on f s

source
theorem continuous_within_at.prod {Ξ± : Type u_1} {Ξ² : Type u_2} {Ξ³ : Type u_3} [topological_space Ξ±] [topological_space Ξ²] [topological_space Ξ³] {f : Ξ± β†’ Ξ²} {g : Ξ± β†’ Ξ³} {s : set Ξ±} {x : Ξ±} :
continuous_within_at f s x β†’ continuous_within_at g s x β†’ continuous_within_at (Ξ» (x : Ξ±), (f x, g x)) s x

source
theorem continuous_on.prod {Ξ± : Type u_1} {Ξ² : Type u_2} {Ξ³ : Type u_3} [topological_space Ξ±] [topological_space Ξ²] [topological_space Ξ³] {f : Ξ± β†’ Ξ²} {g : Ξ± β†’ Ξ³} {s : set Ξ±} :
continuous_on f s β†’ continuous_on g s β†’ continuous_on (Ξ» (x : Ξ±), (f x, g x)) s

source
theorem inducing.continuous_on_iff {Ξ± : Type u_1} {Ξ² : Type u_2} {Ξ³ : Type u_3} [topological_space Ξ±] [topological_space Ξ²] [topological_space Ξ³] {f : Ξ± β†’ Ξ²} {g : Ξ² β†’ Ξ³} (hg : inducing g) {s : set Ξ±} :
continuous_on f s ↔ continuous_on (g ∘ f) s

source
theorem embedding.continuous_on_iff {Ξ± : Type u_1} {Ξ² : Type u_2} {Ξ³ : Type u_3} [topological_space Ξ±] [topological_space Ξ²] [topological_space Ξ³] {f : Ξ± β†’ Ξ²} {g : Ξ² β†’ Ξ³} (hg : embedding g) {s : set Ξ±} :
continuous_on f s ↔ continuous_on (g ∘ f) s

source
theorem continuous_within_at_of_not_mem_closure {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {f : Ξ± β†’ Ξ²} {s : set Ξ±} {x : Ξ±} :
x βˆ‰ closure s β†’ continuous_within_at f s x

source
theorem continuous_on_if' {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {s : set Ξ±} {p : Ξ± β†’ Prop} {f g : Ξ± β†’ Ξ²} {h : Ξ  (a : Ξ±), decidable (p a)} :
(βˆ€ (a : Ξ±), a ∈ s ∩ frontier {a : Ξ± | p a} β†’ filter.tendsto f (𝓝[s ∩ {a : Ξ± | p a}] a) (𝓝 (ite (p a) (f a) (g a)))) β†’ (βˆ€ (a : Ξ±), a ∈ s ∩ frontier {a : Ξ± | p a} β†’ filter.tendsto g (𝓝[s ∩ {a : Ξ± | Β¬p a}] a) (𝓝 (ite (p a) (f a) (g a)))) β†’ continuous_on f (s ∩ {a : Ξ± | p a}) β†’ continuous_on g (s ∩ {a : Ξ± | Β¬p a}) β†’ continuous_on (Ξ» (a : Ξ±), ite (p a) (f a) (g a)) s

source
theorem continuous_on_if {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {p : Ξ± β†’ Prop} {h : Ξ  (a : Ξ±), decidable (p a)} {s : set Ξ±} {f g : Ξ± β†’ Ξ²} :
(βˆ€ (a : Ξ±), a ∈ s ∩ frontier {a : Ξ± | p a} β†’ f a = g a) β†’ continuous_on f (s ∩ closure {a : Ξ± | p a}) β†’ continuous_on g (s ∩ closure {a : Ξ± | Β¬p a}) β†’ continuous_on (Ξ» (a : Ξ±), ite (p a) (f a) (g a)) s

source
theorem continuous_if' {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {p : Ξ± β†’ Prop} {f g : Ξ± β†’ Ξ²} {h : Ξ  (a : Ξ±), decidable (p a)} :
(βˆ€ (a : Ξ±), a ∈ frontier {x : Ξ± | p x} β†’ filter.tendsto f (𝓝[{x : Ξ± | p x}] a) (𝓝 (ite (p a) (f a) (g a)))) β†’ (βˆ€ (a : Ξ±), a ∈ frontier {x : Ξ± | p x} β†’ filter.tendsto g (𝓝[{x : Ξ± | Β¬p x}] a) (𝓝 (ite (p a) (f a) (g a)))) β†’ continuous_on f {x : Ξ± | p x} β†’ continuous_on g {x : Ξ± | Β¬p x} β†’ continuous (Ξ» (a : Ξ±), ite (p a) (f a) (g a))

source
theorem continuous_on_fst {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {s : set (Ξ± Γ— Ξ²)} :
continuous_on prod.fst s

source
theorem continuous_within_at_fst {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {s : set (Ξ± Γ— Ξ²)} {p : Ξ± Γ— Ξ²} :
continuous_within_at prod.fst s p

source
theorem continuous_on_snd {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {s : set (Ξ± Γ— Ξ²)} :
continuous_on prod.snd s

source
theorem continuous_within_at_snd {Ξ± : Type u_1} {Ξ² : Type u_2} [topological_space Ξ±] [topological_space Ξ²] {s : set (Ξ± Γ— Ξ²)} {p : Ξ± Γ— Ξ²} :
continuous_within_at prod.snd s p