mathlib3 documentation

topology.continuous_on

Neighborhoods and continuity relative to a subset #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

@[simp]
theorem nhds_bind_nhds_within {α : Type u_1} [topological_space α] {a : α} {s : set α} :
(nhds a).bind (λ (x : α), nhds_within x s) = nhds_within a s
@[simp]
theorem eventually_nhds_nhds_within {α : Type u_1} [topological_space α] {a : α} {s : set α} {p : α Prop} :
(∀ᶠ (y : α) in nhds a, ∀ᶠ (x : α) in nhds_within y s, p x) ∀ᶠ (x : α) in nhds_within a s, p x
theorem eventually_nhds_within_iff {α : Type u_1} [topological_space α] {a : α} {s : set α} {p : α Prop} :
(∀ᶠ (x : α) in nhds_within a s, p x) ∀ᶠ (x : α) in nhds a, x s p x
theorem frequently_nhds_within_iff {α : Type u_1} [topological_space α] {z : α} {s : set α} {p : α Prop} :
(∃ᶠ (x : α) in nhds_within z s, p x) ∃ᶠ (x : α) in nhds z, p x x s
theorem mem_closure_ne_iff_frequently_within {α : Type u_1} [topological_space α] {z : α} {s : set α} :
z closure (s \ {z}) ∃ᶠ (x : α) in nhds_within z {z}, x s
@[simp]
theorem eventually_nhds_within_nhds_within {α : Type u_1} [topological_space α] {a : α} {s : set α} {p : α Prop} :
(∀ᶠ (y : α) in nhds_within a s, ∀ᶠ (x : α) in nhds_within y s, p x) ∀ᶠ (x : α) in nhds_within a s, p x
theorem nhds_within_eq {α : Type u_1} [topological_space α] (a : α) (s : set α) :
nhds_within a s = (t : set α) (H : t {t : set α | a t is_open t}), filter.principal (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 : (nhds a).has_basis p s) (t : set α) :
(nhds_within a t).has_basis p (λ (i : β), s i t)
theorem nhds_within_basis_open {α : Type u_1} [topological_space α] (a : α) (t : set α) :
(nhds_within a t).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 nhds_within a s (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 nhds_within a s (u : set α) (H : u nhds a), u s t
theorem diff_mem_nhds_within_compl {α : Type u_1} [topological_space α] {x : α} {s : set α} (hs : s nhds x) (t : set α) :
theorem diff_mem_nhds_within_diff {α : Type u_1} [topological_space α] {x : α} {s t : set α} (hs : s nhds_within x t) (t' : set α) :
s \ t' nhds_within x (t \ t')
theorem nhds_of_nhds_within_of_nhds {α : Type u_1} [topological_space α] {s t : set α} {a : α} (h1 : s nhds a) (h2 : t nhds_within a s) :
t nhds a
theorem mem_nhds_within_iff_eventually {α : Type u_1} [topological_space α] {s t : set α} {x : α} :
t nhds_within x s ∀ᶠ (y : α) in nhds x, y s y t
theorem mem_nhds_within_iff_eventually_eq {α : Type u_1} [topological_space α] {s t : set α} {x : α} :
theorem nhds_within_eq_iff_eventually_eq {α : Type u_1} [topological_space α] {s t : set α} {x : α} :
theorem nhds_within_le_iff {α : Type u_1} [topological_space α] {s t : set α} {x : α} :
theorem preimage_nhds_within_coinduced' {α : Type u_1} {β : Type u_2} [topological_space α] {π : α β} {s : set β} {t : set α} {a : α} (h : a t) (ht : is_open t) (hs : s nhds (π a)) :
theorem mem_nhds_within_of_mem_nhds {α : Type u_1} [topological_space α] {s t : set α} {a : α} (h : s nhds a) :
theorem self_mem_nhds_within {α : Type u_1} [topological_space α] {a : α} {s : set α} :
theorem eventually_mem_nhds_within {α : Type u_1} [topological_space α] {a : α} {s : set α} :
∀ᶠ (x : α) in nhds_within a s, x s
theorem inter_mem_nhds_within {α : Type u_1} [topological_space α] (s : set α) {t : set α} {a : α} (h : t nhds a) :
theorem nhds_within_mono {α : Type u_1} [topological_space α] (a : α) {s t : set α} (h : s t) :
theorem pure_le_nhds_within {α : Type u_1} [topological_space α] {a : α} {s : set α} (ha : a s) :
theorem mem_of_mem_nhds_within {α : Type u_1} [topological_space α] {a : α} {s t : set α} (ha : a s) (ht : t nhds_within a s) :
a t
theorem filter.eventually.self_of_nhds_within {α : Type u_1} [topological_space α] {p : α Prop} {s : set α} {x : α} (h : ∀ᶠ (y : α) in nhds_within x s, p y) (hx : x s) :
p x
theorem tendsto_const_nhds_within {α : Type u_1} {β : Type u_2} [topological_space α] {l : filter β} {s : set α} {a : α} (ha : a s) :
filter.tendsto (λ (x : β), a) l (nhds_within a s)
theorem nhds_within_restrict'' {α : Type u_1} [topological_space α] {a : α} (s : set α) {t : set α} (h : t nhds_within a s) :
theorem nhds_within_restrict' {α : Type u_1} [topological_space α] {a : α} (s : set α) {t : set α} (h : t nhds a) :
theorem nhds_within_restrict {α : Type u_1} [topological_space α] {a : α} (s : set α) {t : set α} (h₀ : a t) (h₁ : is_open t) :
theorem nhds_within_le_of_mem {α : Type u_1} [topological_space α] {a : α} {s t : set α} (h : s nhds_within a t) :
theorem nhds_within_le_nhds {α : Type u_1} [topological_space α] {a : α} {s : set α} :
theorem nhds_within_eq_nhds_within' {α : Type u_1} [topological_space α] {a : α} {s t u : set α} (hs : s nhds a) (h₂ : t s = u s) :
theorem nhds_within_eq_nhds_within {α : Type u_1} [topological_space α] {a : α} {s t u : set α} (h₀ : a s) (h₁ : is_open s) (h₂ : t s = u s) :
@[simp]
theorem nhds_within_eq_nhds {α : Type u_1} [topological_space α] {a : α} {s : set α} :
theorem is_open.nhds_within_eq {α : Type u_1} [topological_space α] {a : α} {s : set α} (h : is_open s) (ha : a s) :
theorem preimage_nhds_within_coinduced {α : Type u_1} {β : Type u_2} [topological_space α] {π : α β} {s : set β} {t : set α} {a : α} (h : a t) (ht : is_open t) (hs : s nhds (π a)) :
π ⁻¹' s nhds 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_bUnion {α : Type u_1} [topological_space α] {ι : Type u_2} {I : set ι} (hI : I.finite) (s : ι set α) (a : α) :
nhds_within a ( (i : ι) (H : i I), s i) = (i : ι) (H : i I), nhds_within a (s i)
theorem nhds_within_sUnion {α : Type u_1} [topological_space α] {S : set (set α)} (hS : S.finite) (a : α) :
nhds_within a (⋃₀ S) = (s : set α) (H : s S), nhds_within a s
theorem nhds_within_Union {α : Type u_1} [topological_space α] {ι : Sort u_2} [finite ι] (s : ι set α) (a : α) :
nhds_within a ( (i : ι), s i) = (i : ι), nhds_within a (s i)
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 nhds_within_inter_of_mem {α : Type u_1} [topological_space α] {a : α} {s t : set α} (h : s nhds_within a t) :
theorem nhds_within_inter_of_mem' {α : Type u_1} [topological_space α] {a : α} {s t : set α} (h : s nhds_within a t) :
@[simp]
theorem nhds_within_singleton {α : Type u_1} [topological_space α] (a : α) :
@[simp]
theorem nhds_within_insert {α : Type u_1} [topological_space α] (a : α) (s : set α) :
theorem mem_nhds_within_insert {α : Type u_1} [topological_space α] {a : α} {s t : set α} :
theorem insert_mem_nhds_within_insert {α : Type u_1} [topological_space α] {a : α} {s t : set α} (h : t nhds_within a s) :
theorem insert_mem_nhds_iff {α : Type u_1} [topological_space α] {a : α} {s : set α} :
theorem nhds_within_prod_eq {α : Type u_1} [topological_space α] {β : Type u_2} [topological_space β] (a : α) (b : β) (s : set α) (t : set β) :
nhds_within (a, b) (s ×ˢ t) = (nhds_within a s).prod (nhds_within b t)
theorem nhds_within_prod {α : Type u_1} [topological_space α] {β : Type u_2} [topological_space β] {s u : set α} {t v : set β} {a : α} {b : β} (hu : u nhds_within a s) (hv : v nhds_within b t) :
u ×ˢ v nhds_within (a, b) (s ×ˢ t)
theorem nhds_within_pi_eq' {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), topological_space (α i)] {I : set ι} (hI : I.finite) (s : Π (i : ι), set (α i)) (x : Π (i : ι), α i) :
nhds_within x (I.pi s) = (i : ι), filter.comap (λ (x : Π (i : ι), α i), x i) (nhds (x i) (hi : i I), filter.principal (s i))
theorem nhds_within_pi_eq {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), topological_space (α i)] {I : set ι} (hI : I.finite) (s : Π (i : ι), set (α i)) (x : Π (i : ι), α i) :
nhds_within x (I.pi s) = ( (i : ι) (H : i I), filter.comap (λ (x : Π (i : ι), α i), x i) (nhds_within (x i) (s i))) (i : ι) (H : i I), filter.comap (λ (x : Π (i : ι), α i), x i) (nhds (x i))
theorem nhds_within_pi_univ_eq {ι : Type u_1} {α : ι Type u_2} [finite ι] [Π (i : ι), topological_space (α i)] (s : Π (i : ι), set (α i)) (x : Π (i : ι), α i) :
nhds_within x (set.univ.pi s) = (i : ι), filter.comap (λ (x : Π (i : ι), α i), x i) (nhds_within (x i) (s i))
theorem nhds_within_pi_eq_bot {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), topological_space (α i)] {I : set ι} {s : Π (i : ι), set (α i)} {x : Π (i : ι), α i} :
nhds_within x (I.pi s) = (i : ι) (H : i I), nhds_within (x i) (s i) =
theorem nhds_within_pi_ne_bot {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), topological_space (α i)] {I : set ι} {s : Π (i : ι), set (α i)} {x : Π (i : ι), α i} :
(nhds_within x (I.pi s)).ne_bot (i : ι), i I (nhds_within (x i) (s i)).ne_bot
theorem filter.tendsto.piecewise_nhds_within {α : Type u_1} {β : Type u_2} [topological_space α] {f g : α β} {t : set α} [Π (x : α), decidable (x t)] {a : α} {s : set α} {l : filter β} (h₀ : filter.tendsto f (nhds_within a (s t)) l) (h₁ : filter.tendsto g (nhds_within a (s t)) l) :
theorem filter.tendsto.if_nhds_within {α : Type u_1} {β : Type u_2} [topological_space α] {f g : α β} {p : α Prop} [decidable_pred p] {a : α} {s : set α} {l : filter β} (h₀ : filter.tendsto f (nhds_within a (s {x : α | p x})) l) (h₁ : filter.tendsto g (nhds_within a (s {x : α | ¬p x})) l) :
filter.tendsto (λ (x : α), ite (p x) (f x) (g x)) (nhds_within a s) l
theorem map_nhds_within {α : Type u_1} {β : Type u_2} [topological_space α] (f : α β) (a : α) (s : set α) :
filter.map f (nhds_within a s) = (t : set α) (H : t {t : set α | a t is_open t}), filter.principal (f '' (t s))
theorem tendsto_nhds_within_mono_left {α : Type u_1} {β : Type u_2} [topological_space α] {f : α β} {a : α} {s t : set α} {l : filter β} (hst : s t) (h : filter.tendsto f (nhds_within a t) l) :
theorem tendsto_nhds_within_mono_right {α : Type u_1} {β : Type u_2} [topological_space α] {f : β α} {l : filter β} {a : α} {s t : set α} (hst : s t) (h : filter.tendsto f l (nhds_within a s)) :
theorem tendsto_nhds_within_of_tendsto_nhds {α : Type u_1} {β : Type u_2} [topological_space α] {f : α β} {a : α} {s : set α} {l : filter β} (h : filter.tendsto f (nhds a) l) :
theorem eventually_mem_of_tendsto_nhds_within {α : Type u_1} {β : Type u_2} [topological_space α] {f : β α} {a : α} {s : set α} {l : filter β} (h : filter.tendsto f l (nhds_within a s)) :
∀ᶠ (i : β) in l, f i s
theorem tendsto_nhds_of_tendsto_nhds_within {α : Type u_1} {β : Type u_2} [topological_space α] {f : β α} {a : α} {s : set α} {l : filter β} (h : filter.tendsto f l (nhds_within a s)) :
theorem principal_subtype {α : Type u_1} (s : set α) (t : set {x // x s}) :
theorem nhds_within_ne_bot_of_mem {α : Type u_1} [topological_space α] {s : set α} {x : α} (hx : x s) :
theorem is_closed.mem_of_nhds_within_ne_bot {α : Type u_1} [topological_space α] {s : set α} (hs : is_closed s) {x : α} (hx : (nhds_within x s).ne_bot) :
x s
theorem dense_range.nhds_within_ne_bot {α : Type u_1} [topological_space α] {ι : Type u_2} {f : ι α} (h : dense_range f) (x : α) :
theorem mem_closure_pi {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), topological_space (α i)] {I : set ι} {s : Π (i : ι), set (α i)} {x : Π (i : ι), α i} :
x closure (I.pi s) (i : ι), i I x i closure (s i)
theorem closure_pi_set {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), topological_space (α i)] (I : set ι) (s : Π (i : ι), set (α i)) :
closure (I.pi s) = I.pi (λ (i : ι), closure (s i))
theorem dense_pi {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), topological_space (α i)] {s : Π (i : ι), set (α i)} (I : set ι) (hs : (i : ι), i I dense (s i)) :
dense (I.pi s)
theorem eventually_eq_nhds_within_iff {α : Type u_1} {β : Type u_2} [topological_space α] {f g : α β} {s : set α} {a : α} :
f =ᶠ[nhds_within a s] g ∀ᶠ (x : α) in nhds a, x s f x = g x
theorem eventually_eq_nhds_within_of_eq_on {α : Type u_1} {β : Type u_2} [topological_space α] {f g : α β} {s : set α} {a : α} (h : set.eq_on f g s) :
theorem set.eq_on.eventually_eq_nhds_within {α : Type u_1} {β : Type u_2} [topological_space α] {f g : α β} {s : set α} {a : α} (h : set.eq_on f g s) :
theorem tendsto_nhds_within_congr {α : Type u_1} {β : Type u_2} [topological_space α] {f g : α β} {s : set α} {a : α} {l : filter β} (hfg : (x : α), x s f x = g x) (hf : filter.tendsto f (nhds_within a s) l) :
theorem eventually_nhds_within_of_forall {α : Type u_1} [topological_space α] {s : set α} {a : α} {p : α Prop} (h : (x : α), x s p x) :
∀ᶠ (x : α) in nhds_within a s, p x
theorem tendsto_nhds_within_of_tendsto_nhds_of_eventually_within {α : Type u_1} {β : Type u_2} [topological_space α] {a : α} {l : filter β} {s : set α} (f : β α) (h1 : filter.tendsto f l (nhds a)) (h2 : ∀ᶠ (x : β) in l, f x s) :
theorem tendsto_nhds_within_iff {α : Type u_1} {β : Type u_2} [topological_space α] {a : α} {l : filter β} {s : set α} {f : β α} :
filter.tendsto f l (nhds_within a s) filter.tendsto f l (nhds a) ∀ᶠ (n : β) in l, f n s
@[simp]
theorem tendsto_nhds_within_range {α : Type u_1} {β : Type u_2} [topological_space α] {a : α} {l : filter β} {f : β α} :
theorem filter.eventually_eq.eq_of_nhds_within {α : Type u_1} {β : Type u_2} [topological_space α] {s : set α} {f g : α β} {a : α} (h : f =ᶠ[nhds_within a s] g) (hmem : a s) :
f a = g a
theorem eventually_nhds_within_of_eventually_nhds {α : Type u_1} [topological_space α] {s : set α} {a : α} {p : α Prop} (h : ∀ᶠ (x : α) in nhds a, p x) :
∀ᶠ (x : α) in nhds_within a s, 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 mem_nhds_subtype_iff_nhds_within {α : Type u_1} [topological_space α] {s : set α} {a : s} {t : set s} :
theorem preimage_coe_mem_nhds_subtype {α : Type u_1} [topological_space α] {s t : set α} {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 β] (f : α β) (s : set α) (x : α) :
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 : α} (h : continuous_within_at f s 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 β] (f : α β) (s : 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 : α} (hf : continuous_on f s) (hx : x s) :
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 {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {x : α} {s : set α} {t : set β} (h : continuous_within_at f s x) (ht : set.maps_to f s t) :
theorem continuous_within_at.tendsto_nhds_within_image {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {x : α} {s : set α} (h : continuous_within_at f s x) :
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 : β} (hf : continuous_within_at f s x) (hg : continuous_within_at g t y) :
theorem continuous_within_at_pi {α : Type u_1} [topological_space α] {ι : Type u_2} {π : ι Type u_3} [Π (i : ι), topological_space (π i)] {f : α Π (i : ι), π i} {s : set α} {x : α} :
continuous_within_at f s x (i : ι), continuous_within_at (λ (y : α), f y i) s x
theorem continuous_on_pi {α : Type u_1} [topological_space α] {ι : Type u_2} {π : ι Type u_3} [Π (i : ι), topological_space (π i)] {f : α Π (i : ι), π i} {s : set α} :
continuous_on f s (i : ι), continuous_on (λ (y : α), f y i) s
theorem continuous_within_at.fin_insert_nth {α : Type u_1} [topological_space α] {n : } {π : fin (n + 1) Type u_2} [Π (i : fin (n + 1)), topological_space (π i)] (i : fin (n + 1)) {f : α π i} {a : α} {s : set α} (hf : continuous_within_at f s a) {g : α Π (j : fin n), π ((i.succ_above) j)} (hg : continuous_within_at g s a) :
continuous_within_at (λ (a : α), i.insert_nth (f a) (g a)) s a
theorem continuous_on.fin_insert_nth {α : Type u_1} [topological_space α] {n : } {π : fin (n + 1) Type u_2} [Π (i : fin (n + 1)), topological_space (π i)] (i : fin (n + 1)) {f : α π i} {s : set α} (hf : continuous_on f s) {g : α Π (j : fin n), π ((i.succ_above) j)} (hg : continuous_on g s) :
continuous_on (λ (a : α), i.insert_nth (f a) (g a)) s
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)
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.mono_dom {α : Type u_1} {β : Type u_2} {t₁ t₂ : topological_space α} {t₃ : topological_space β} (h₁ : t₂ t₁) {s : set α} {f : α β} (h₂ : continuous_on 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 continuous_on.mono_rng {α : Type u_1} {β : Type u_2} {t₁ : topological_space α} {t₂ t₃ : topological_space β} (h₁ : t₂ t₃) {s : set α} {f : α β} (h₂ : continuous_on 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 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 β} (hf : continuous_on f s) (hg : continuous_on g t) :
theorem continuous_of_cover_nhds {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {ι : Sort u_3} {f : α β} {s : ι set α} (hs : (x : α), (i : ι), s i nhds x) (hf : (i : ι), continuous_on f (s i)) :
theorem continuous_on_empty {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α β) :
theorem continuous_on_singleton {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α β) (a : α) :
theorem set.subsingleton.continuous_on {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set α} (hs : s.subsingleton) (f : α β) :
theorem nhds_within_le_comap {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {x : α} {s : set α} {f : α β} (ctsf : continuous_within_at f s x) :
@[simp]
theorem comap_nhds_within_range {β : Type u_2} [topological_space β] {α : Type u_1} (f : α β) (y : β) :
theorem continuous_within_at.mono {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s t : set α} {x : α} (h : continuous_within_at f t x) (hs : s t) :
theorem continuous_within_at.mono_of_mem {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s t : set α} {x : α} (h : continuous_within_at f t x) (hs : t nhds_within x s) :
theorem continuous_within_at_inter' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s t : set α} {x : α} (h : t nhds_within x s) :
theorem continuous_within_at_inter {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s t : set α} {x : α} (h : t nhds 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.union {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s t : set α} {x : α} (hs : continuous_within_at f s x) (ht : continuous_within_at f t x) :
theorem continuous_within_at.mem_closure_image {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} {x : α} (h : continuous_within_at f s x) (hx : x closure s) :
f 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 β} (h : continuous_within_at f s x) (hx : x closure s) (hA : set.maps_to f s A) :
f x closure A
theorem set.maps_to.closure_of_continuous_within_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} {t : set β} (h : set.maps_to f s t) (hc : (x : α), x closure s continuous_within_at f s x) :
theorem set.maps_to.closure_of_continuous_on {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} {t : set β} (h : set.maps_to f s t) (hc : continuous_on f (closure s)) :
theorem continuous_within_at.image_closure {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} (hf : (x : α), x closure s continuous_within_at f s x) :
f '' closure s closure (f '' s)
theorem continuous_on.image_closure {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} (hf : continuous_on f (closure s)) :
f '' closure s closure (f '' s)
@[simp]
theorem continuous_within_at_singleton {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {x : α} :
@[simp]
theorem continuous_within_at_insert_self {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {x : α} {s : set α} :
theorem continuous_within_at.insert_self {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {x : α} {s : set α} :

Alias of the reverse direction of continuous_within_at_insert_self.

theorem continuous_within_at.diff_iff {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s t : set α} {x : α} (ht : continuous_within_at f t x) :
@[simp]
theorem continuous_within_at_diff_self {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} {x : α} :
@[simp]
theorem continuous_within_at_compl_self {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {a : α} :
@[simp]
theorem continuous_within_at_update_same {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [decidable_eq α] {f : α β} {s : set α} {x : α} {y : β} :
@[simp]
theorem continuous_at_update_same {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [decidable_eq α] {f : α β} {x : α} {y : β} :
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 (s.restrict f)) {finv : β α} (hleft : set.left_inv_on finv f s) :
continuous_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 : β α} (hleft : function.left_inverse finv f) :
theorem continuous_on.congr_mono {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : α β} {s s₁ : set α} (h : continuous_on f s) (h' : set.eq_on g f s₁) (h₁ : s₁ s) :
theorem continuous_on.congr {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : α β} {s : set α} (h : continuous_on f s) (h' : set.eq_on g f s) :
theorem continuous_on_congr {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : α β} {s : set α} (h' : set.eq_on g f s) :
theorem continuous_at.continuous_within_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} {x : α} (h : continuous_at f x) :
theorem continuous_within_at_iff_continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} {x : α} (h : s nhds x) :
theorem continuous_within_at.continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} {x : α} (h : continuous_within_at f s x) (hs : s nhds x) :
theorem is_open.continuous_on_iff {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} (hs : is_open s) :
continuous_on f s ⦃a : α⦄, a s continuous_at f a
theorem continuous_on.continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} {x : α} (h : continuous_on f s) (hx : s nhds x) :
theorem continuous_at.continuous_on {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} (hcont : (x : α), x s continuous_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 : α} (hg : continuous_within_at g t (f x)) (hf : continuous_within_at f s x) (h : set.maps_to f s t) :
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 : α} (hg : continuous_within_at g t (f x)) (hf : continuous_within_at f s x) :
theorem continuous_at.comp_continuous_within_at {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β γ} {f : α β} {s : set α} {x : α} (hg : continuous_at g (f x)) (hf : continuous_within_at f s 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 β} (hg : continuous_on g t) (hf : continuous_on f s) (h : set.maps_to f s t) :
theorem continuous_on.mono {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s t : set α} (hf : continuous_on f s) (h : t s) :
theorem antitone_continuous_on {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} :
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 β} (hg : continuous_on g t) (hf : continuous_on f s) :
continuous_on (g f) (s f ⁻¹' t)
theorem continuous.continuous_on {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} (h : continuous f) :
theorem continuous.continuous_within_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} {x : α} (h : continuous f) :
theorem continuous.comp_continuous_on {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β γ} {f : α β} {s : set α} (hg : continuous g) (hf : continuous_on f s) :
theorem continuous_on.comp_continuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β γ} {f : α β} {s : set β} (hg : continuous_on g s) (hf : continuous f) (hs : (x : α), f x s) :
theorem continuous_within_at.preimage_mem_nhds_within {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {x : α} {s : set α} {t : set β} (h : continuous_within_at f s x) (ht : t nhds (f x)) :
theorem set.left_inv_on.map_nhds_within_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {g : β α} {x : β} {s : set β} (h : set.left_inv_on f g s) (hx : f (g x) = x) (hf : continuous_within_at f (g '' s) (g x)) (hg : continuous_within_at g s x) :
filter.map g (nhds_within x s) = nhds_within (g x) (g '' s)
theorem function.left_inverse.map_nhds_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {g : β α} {x : β} (h : function.left_inverse f g) (hf : continuous_within_at f (set.range g) (g x)) (hg : continuous_at g 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 β} (h : continuous_within_at f s x) (ht : t nhds_within (f x) (f '' s)) :
theorem filter.eventually_eq.congr_continuous_within_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : α β} {s : set α} {x : α} (h : f =ᶠ[nhds_within x s] g) (hx : f x = g x) :
theorem continuous_within_at.congr_of_eventually_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f f₁ : α β} {s : set α} {x : α} (h : continuous_within_at f s x) (h₁ : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) :
theorem continuous_within_at.congr {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f f₁ : α β} {s : set α} {x : α} (h : continuous_within_at f s x) (h₁ : (y : α), y s f₁ y = f y) (hx : f₁ x = f x) :
theorem continuous_within_at.congr_mono {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : α β} {s s₁ : set α} {x : α} (h : continuous_within_at f s x) (h' : set.eq_on g f s₁) (h₁ : s₁ s) (hx : g x = f 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 α} (hs : is_open s) :
continuous_on f s (t : set β), is_open t is_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 β} (hf : continuous_on f s) (hs : is_open s) (ht : is_open t) :
theorem continuous_on.is_open_preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} {t : set β} (h : continuous_on f s) (hs : is_open s) (hp : f ⁻¹' t s) (ht : is_open t) :
theorem continuous_on.preimage_closed_of_closed {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} {t : set β} (hf : continuous_on f s) (hs : is_closed s) (ht : is_closed t) :
theorem continuous_on.preimage_interior_subset_interior_preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} {t : set β} (hf : continuous_on f s) (hs : is_open s) :
theorem continuous_on_of_locally_continuous_on {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} {s : set α} (h : (x : α), x s ( (t : set α), is_open t x t continuous_on f (s t))) :
theorem continuous_on_open_of_generate_from {α : Type u_1} [topological_space α] {β : Type u_2} {s : set α} {T : set (set β)} {f : α β} (hs : is_open s) (h : (t : set β), t T is_open (s f ⁻¹' t)) :
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 : α} (hf : continuous_within_at f s x) (hg : continuous_within_at g s x) :
continuous_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 α} (hf : continuous_on f s) (hg : continuous_on g s) :
continuous_on (λ (x : α), (f x, g x)) s
theorem inducing.continuous_within_at_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α β} {g : β γ} (hg : inducing g) {s : set α} {x : α} :
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 embedding.map_nhds_within_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} (hf : embedding f) (s : set α) (x : α) :
filter.map f (nhds_within x s) = nhds_within (f x) (f '' s)
theorem open_embedding.map_nhds_within_preimage_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α β} (hf : open_embedding f) (s : set β) (x : α) :
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.piecewise' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s t : set α} {f g : α β} [Π (a : α), decidable (a t)] (hpf : (a : α), a s frontier t filter.tendsto f (nhds_within a (s t)) (nhds (t.piecewise f g a))) (hpg : (a : α), a s frontier t filter.tendsto g (nhds_within a (s t)) (nhds (t.piecewise f g a))) (hf : continuous_on f (s t)) (hg : continuous_on g (s t)) :
theorem continuous_on.if' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set α} {p : α Prop} {f g : α β} [Π (a : α), decidable (p a)] (hpf : (a : α), a s frontier {a : α | p a} filter.tendsto f (nhds_within a (s {a : α | p a})) (nhds (ite (p a) (f a) (g a)))) (hpg : (a : α), a s frontier {a : α | p a} filter.tendsto g (nhds_within a (s {a : α | ¬p a})) (nhds (ite (p a) (f a) (g a)))) (hf : continuous_on f (s {a : α | p a})) (hg : 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} [Π (a : α), decidable (p a)] {s : set α} {f g : α β} (hp : (a : α), a s frontier {a : α | p a} f a = g a) (hf : continuous_on f (s closure {a : α | p a})) (hg : continuous_on g (s closure {a : α | ¬p a})) :
continuous_on (λ (a : α), ite (p a) (f a) (g a)) s
theorem continuous_on.piecewise {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s t : set α} {f g : α β} [Π (a : α), decidable (a t)] (ht : (a : α), a s frontier t f a = g a) (hf : continuous_on f (s closure t)) (hg : continuous_on g (s closure t)) :
theorem continuous_if' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {p : α Prop} {f g : α β} [Π (a : α), decidable (p a)] (hpf : (a : α), a frontier {x : α | p x} filter.tendsto f (nhds_within a {x : α | p x}) (nhds (ite (p a) (f a) (g a)))) (hpg : (a : α), a frontier {x : α | p x} filter.tendsto g (nhds_within a {x : α | ¬p x}) (nhds (ite (p a) (f a) (g a)))) (hf : continuous_on f {x : α | p x}) (hg : continuous_on g {x : α | ¬p x}) :
continuous (λ (a : α), ite (p a) (f a) (g a))
theorem continuous_if {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {p : α Prop} {f g : α β} [Π (a : α), decidable (p a)] (hp : (a : α), a frontier {x : α | p x} f a = g a) (hf : continuous_on f (closure {x : α | p x})) (hg : continuous_on g (closure {x : α | ¬p x})) :
continuous (λ (a : α), ite (p a) (f a) (g a))
theorem continuous.if {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {p : α Prop} {f g : α β} [Π (a : α), decidable (p a)] (hp : (a : α), a frontier {x : α | p x} f a = g a) (hf : continuous f) (hg : continuous g) :
continuous (λ (a : α), ite (p a) (f a) (g a))
theorem continuous_if_const {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (p : Prop) {f g : α β} [decidable p] (hf : p continuous f) (hg : ¬p continuous g) :
continuous (λ (a : α), ite p (f a) (g a))
theorem continuous.if_const {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (p : Prop) {f g : α β} [decidable p] (hf : continuous f) (hg : continuous g) :
continuous (λ (a : α), ite p (f a) (g a))
theorem continuous_piecewise {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set α} {f g : α β} [Π (a : α), decidable (a s)] (hs : (a : α), a frontier s f a = g a) (hf : continuous_on f (closure s)) (hg : continuous_on g (closure s)) :
theorem continuous.piecewise {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set α} {f g : α β} [Π (a : α), decidable (a s)] (hs : (a : α), a frontier s f a = g a) (hf : continuous f) (hg : continuous g) :
theorem is_open.ite' {α : Type u_1} [topological_space α] {s s' t : set α} (hs : is_open s) (hs' : is_open s') (ht : (x : α), x frontier t (x s x s')) :
is_open (t.ite s s')
theorem is_open.ite {α : Type u_1} [topological_space α] {s s' t : set α} (hs : is_open s) (hs' : is_open s') (ht : s frontier t = s' frontier t) :
is_open (t.ite s s')
theorem ite_inter_closure_eq_of_inter_frontier_eq {α : Type u_1} [topological_space α] {s s' 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} [topological_space α] {s s' t : set α} (ht : s frontier t = s' frontier t) :
theorem continuous_on_piecewise_ite' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s s' t : set α} {f f' : α β} [Π (x : α), decidable (x t)] (h : continuous_on f (s closure t)) (h' : continuous_on f' (s' closure t)) (H : s frontier t = s' frontier t) (Heq : set.eq_on f f' (s frontier t)) :
continuous_on (t.piecewise f f') (t.ite s s')
theorem continuous_on_piecewise_ite {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s s' t : set α} {f f' : α β} [Π (x : α), decidable (x t)] (h : continuous_on f s) (h' : continuous_on f' s') (H : s frontier t = s' frontier t) (Heq : set.eq_on f f' (s frontier t)) :
continuous_on (t.piecewise f f') (t.ite s s')
theorem frontier_inter_open_inter {α : Type u_1} [topological_space α] {s t : set α} (ht : is_open t) :
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.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α β × γ} {s : set α} (hf : continuous_on f s) :
continuous_on (λ (x : α), (f x).fst) s
theorem continuous_within_at.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α β × γ} {s : set α} {a : α} (h : continuous_within_at f s a) :
continuous_within_at (λ (x : α), (f x).fst) s a
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 : α × β} :
theorem continuous_on.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α β × γ} {s : set α} (hf : continuous_on f s) :
continuous_on (λ (x : α), (f x).snd) s
theorem continuous_within_at.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α β × γ} {s : set α} {a : α} (h : continuous_within_at f s a) :
continuous_within_at (λ (x : α), (f x).snd) s a
theorem continuous_within_at_prod_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α β × γ} {s : set α} {x : α} :