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

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
@[simp]
theorem nhds_bind_nhds_within {α : Type u_1} [topological_space α] {a : α} {s : set α} :
(𝓝 a).bind (λ (x : α), 𝓝[s] x) = 𝓝[s] a

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

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

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

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)

theorem nhds_within_univ {α : Type u_1} [topological_space α] (a : α) :

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)

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)

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

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

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

theorem nhds_of_nhds_within_of_nhds {α : Type u_1} [topological_space α] {s t : set α} {a : α} :
s 𝓝 at 𝓝[s] at 𝓝 a

theorem mem_nhds_within_of_mem_nhds {α : Type u_1} [topological_space α] {s t : set α} {a : α} :
s 𝓝 as 𝓝[t] a

theorem self_mem_nhds_within {α : Type u_1} [topological_space α] {a : α} {s : set α} :
s 𝓝[s] a

theorem inter_mem_nhds_within {α : Type u_1} [topological_space α] (s : set α) {t : set α} {a : α} :
t 𝓝 as t 𝓝[s] a

theorem nhds_within_mono {α : Type u_1} [topological_space α] (a : α) {s t : set α} :
s t𝓝[s] a 𝓝[t] a

theorem pure_le_nhds_within {α : Type u_1} [topological_space α] {a : α} {s : set α} :
a spure a 𝓝[s] a

theorem mem_of_mem_nhds_within {α : Type u_1} [topological_space α] {a : α} {s t : set α} :
a st 𝓝[s] aa t

theorem filter.eventually.self_of_nhds_within {α : Type u_1} [topological_space α] {p : α → Prop} {s : set α} {x : α} :
(∀ᶠ (y : α) in 𝓝[s] x, p y)x sp x

theorem tendsto_const_nhds_within {α : Type u_1} {β : Type u_2} [topological_space α] {l : filter β} {s : set α} {a : α} :
a sfilter.tendsto (λ (x : β), a) l (𝓝[s] a)

theorem nhds_within_restrict'' {α : Type u_1} [topological_space α] {a : α} (s : set α) {t : set α} :
t 𝓝[s] a𝓝[s] a = 𝓝[s t] a

theorem nhds_within_restrict' {α : Type u_1} [topological_space α] {a : α} (s : set α) {t : set α} :
t 𝓝 a𝓝[s] a = 𝓝[s t] a

theorem nhds_within_restrict {α : Type u_1} [topological_space α] {a : α} (s : set α) {t : set α} :
a tis_open t𝓝[s] a = 𝓝[s t] a

theorem nhds_within_le_of_mem {α : Type u_1} [topological_space α] {a : α} {s t : set α} :
s 𝓝[t] a𝓝[t] a 𝓝[s] a

theorem nhds_within_eq_nhds_within {α : Type u_1} [topological_space α] {a : α} {s t u : set α} :
a sis_open st s = u s𝓝[t] a = 𝓝[u] a

theorem nhds_within_eq_of_open {α : Type u_1} [topological_space α] {a : α} {s : set α} :
a sis_open s𝓝[s] a = 𝓝 a

@[simp]
theorem nhds_within_empty {α : Type u_1} [topological_space α] (a : α) :

theorem nhds_within_union {α : Type u_1} [topological_space α] (a : α) (s t : set α) :

theorem nhds_within_inter {α : Type u_1} [topological_space α] (a : α) (s t : set α) :

theorem nhds_within_inter' {α : Type u_1} [topological_space α] (a : α) (s t : set α) :

theorem mem_nhds_within_insert {α : Type u_1} [topological_space α] {a : α} {s t : set α} :
t 𝓝[s] ainsert a t 𝓝[insert a s] a

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

theorem nhds_within_prod {α : Type u_1} [topological_space α] {β : Type u_2} [topological_space β] {s u : set α} {t v : set β} {a : α} {b : β} :
u 𝓝[s] av 𝓝[t] bu.prod v 𝓝[s.prod t] (a, b)

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) lfilter.tendsto g (𝓝[s {x : α | ¬p x}] a) lfilter.tendsto (λ (x : α), ite (p x) (f x) (g x)) (𝓝[s] a) l

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

theorem tendsto_nhds_within_mono_left {α : Type u_1} {β : Type u_2} [topological_space α] {f : α → β} {a : α} {s t : set α} {l : filter β} :
s tfilter.tendsto f (𝓝[t] a) lfilter.tendsto f (𝓝[s] a) l

theorem tendsto_nhds_within_mono_right {α : Type u_1} {β : Type u_2} [topological_space α] {f : β → α} {l : filter β} {a : α} {s t : set α} :
s tfilter.tendsto f l (𝓝[s] a)filter.tendsto f l (𝓝[t] a)

theorem tendsto_nhds_within_of_tendsto_nhds {α : Type u_1} {β : Type u_2} [topological_space α] {f : α → β} {a : α} {s : set α} {l : filter β} :

theorem principal_subtype {α : Type u_1} (s : set α) (t : set {x // x s}) :

theorem mem_closure_iff_nhds_within_ne_bot {α : Type u_1} [topological_space α] {s : set α} {x : α} :

theorem nhds_within_ne_bot_of_mem {α : Type u_1} [topological_space α] {s : set α} {x : α} :
x s(𝓝[s] x).ne_bot

theorem is_closed.mem_of_nhds_within_ne_bot {α : Type u_1} [topological_space α] {s : set α} (hs : is_closed s) {x : α} :
(𝓝[s] x).ne_botx s

theorem dense_range.nhds_within_ne_bot {α : Type u_1} [topological_space α] {ι : Type u_2} {f : ι → α} (h : dense_range f) (x : α) :

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 sf x = g x

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 sf =ᶠ[𝓝[s] a] g

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 sf =ᶠ[𝓝[s] a] g

theorem tendsto_nhds_within_congr {α : Type u_1} {β : Type u_2} [topological_space α] {f g : α → β} {s : set α} {a : α} {l : filter β} :
(∀ (x : α), x sf x = g x)filter.tendsto f (𝓝[s] a) lfilter.tendsto g (𝓝[s] a) l

theorem eventually_nhds_with_of_forall {α : Type u_1} [topological_space α] {s : set α} {a : α} {p : α → Prop} :
(∀ (x : α), x sp x)(∀ᶠ (x : α) in 𝓝[s] a, p x)

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)

theorem filter.eventually_eq.eq_of_nhds_within {α : Type u_1} {β : Type u_2} [topological_space α] {s : set α} {f g : α → β} {a : α} :
f =ᶠ[𝓝[s] a] ga sf a = g a

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

theorem mem_nhds_within_subtype {α : Type u_1} [topological_space α] {s : set α} {a : {x // x s}} {t u : set {x // x s}} :

theorem nhds_within_subtype {α : Type u_1} [topological_space α] (s : set α) (a : {x // x s}) (t : set {x // x s}) :

theorem nhds_within_eq_map_subtype_coe {α : Type u_1} [topological_space α] {s : set α} {a : α} (h : a s) :

theorem tendsto_nhds_within_iff_subtype {α : Type u_1} {β : Type u_2} [topological_space α] {s : set α} {a : α} (h : a s) (f : α → β) (l : filter β) :

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
theorem continuous_within_at.tendsto {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {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.

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
theorem continuous_on.continuous_within_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {x : α} :
continuous_on f sx scontinuous_within_at f s x

theorem continuous_within_at_univ {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) (x : α) :

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

theorem continuous_within_at.tendsto_nhds_within_image {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} {s : set α} :

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 : β} :

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 tf x t(∃ (u : set α), is_open u x u u s f ⁻¹' t)

theorem continuous_on_iff_continuous_restrict {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} :

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)

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)

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 β} :

theorem continuous_on_empty {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) :

theorem nhds_within_le_comap {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {x : α} {s : set α} {f : α → β} :

theorem continuous_within_at_iff_ptendsto_res {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) {x : α} {s : set α} :

theorem continuous_iff_continuous_on_univ {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :

theorem continuous_within_at.mono {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s t : set α} {x : α} :

theorem continuous_within_at_inter' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s t : set α} {x : α} :

theorem continuous_within_at_inter {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s t : set α} {x : α} :

theorem continuous_within_at.union {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s t : set α} {x : α} :

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 xx closure sf x closure (f '' s)

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 xx closure ss f ⁻¹' Af x closure A

theorem continuous_within_at.image_closure {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} :
(∀ (x : α), x closure scontinuous_within_at f s x)f '' closure s closure (f '' s)

theorem continuous_within_at_singleton {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} :

theorem continuous_within_at.diff_iff {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s t : set α} {x : α} :

@[simp]
theorem continuous_within_at_diff_self {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {x : α} :

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 scontinuous_on finv (f '' s)

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 : β → α} :

theorem continuous_on.congr_mono {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : α → β} {s s₁ : set α} :
continuous_on f sset.eq_on g f s₁s₁ scontinuous_on g s₁

theorem continuous_on.congr {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : α → β} {s : set α} :
continuous_on f sset.eq_on g f scontinuous_on g s

theorem continuous_on_congr {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : α → β} {s : set α} :

theorem continuous_at.continuous_within_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {x : α} :

theorem continuous_within_at.continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {x : α} :

theorem continuous_on.continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {x : α} :
continuous_on f ss 𝓝 xcontinuous_at f x

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 xs f ⁻¹' tcontinuous_within_at (g f) s x

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 : α} :

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 tcontinuous_on f ss f ⁻¹' tcontinuous_on (g f) s

theorem continuous_on.mono {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s t : set α} :
continuous_on f st scontinuous_on f t

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 tcontinuous_on f scontinuous_on (g f) (s f ⁻¹' t)

theorem continuous.continuous_on {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} :

theorem continuous.continuous_within_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {x : α} :

theorem continuous.comp_continuous_on {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} {s : set α} :

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 scontinuous fset.range f scontinuous (g f)

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 xt 𝓝 (f x)f ⁻¹' t 𝓝[s] x

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 xt 𝓝[f '' s] f xf ⁻¹' t 𝓝[s] x

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 xf₁ =ᶠ[𝓝[s] x] ff₁ x = f xcontinuous_within_at f₁ s x

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 sf₁ y = f y)f₁ x = f xcontinuous_within_at f₁ s x

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 xset.eq_on g f s₁s₁ sg x = f xcontinuous_within_at g s₁ x

theorem continuous_on_const {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set α} {c : β} :
continuous_on (λ (x : α), c) s

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

theorem continuous_on_id {α : Type u_1} [topological_space α] {s : set α} :

theorem continuous_within_at_id {α : Type u_1} [topological_space α] {s : set α} {x : α} :

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 tis_open (s f ⁻¹' t))

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 sis_open sis_open tis_open (s f ⁻¹' t)

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 sis_closed sis_closed tis_closed (s f ⁻¹' t)

theorem continuous_on.preimage_interior_subset_interior_preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {t : set β} :

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

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 Tis_open (s f ⁻¹' t))continuous_on f s

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 xcontinuous_within_at g s xcontinuous_within_at (λ (x : α), (f x, g x)) s x

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 scontinuous_on g scontinuous_on (λ (x : α), (f x, g x)) s

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 α} :

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 α} :

theorem continuous_within_at_of_not_mem_closure {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {x : α} :

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

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

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

theorem continuous_on_fst {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set × β)} :

theorem continuous_within_at_fst {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set × β)} {p : α × β} :

theorem continuous_on_snd {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set × β)} :

theorem continuous_within_at_snd {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set × β)} {p : α × β} :