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 #

@[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 {α : Type u_1} [topological_space α] {x : α} {s : set α} (hs : s 𝓝 x) (t : set α) :
s \ t 𝓝[t] x
theorem diff_mem_nhds_within_diff {α : Type u_1} [topological_space α] {x : α} {s t : set α} (hs : s 𝓝[t] x) (t' : set α) :
s \ t' 𝓝[t \ t'] x
theorem nhds_of_nhds_within_of_nhds {α : Type u_1} [topological_space α] {s t : set α} {a : α} (h1 : s 𝓝 a) (h2 : t 𝓝[s] a) :
t 𝓝 a
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 𝓝 (π a)) :
π ⁻¹' s 𝓝[t] a
theorem mem_nhds_within_of_mem_nhds {α : Type u_1} [topological_space α] {s t : set α} {a : α} (h : s 𝓝 a) :
s 𝓝[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 : α} (h : t 𝓝 a) :
s t 𝓝[s] 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 𝓝[s] a) :
a t
theorem filter.eventually.self_of_nhds_within {α : Type u_1} [topological_space α] {p : α → Prop} {s : set α} {x : α} (h : ∀ᶠ (y : α) in 𝓝[s] x, 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 (𝓝[s] a)
theorem nhds_within_restrict'' {α : Type u_1} [topological_space α] {a : α} (s : set α) {t : set α} (h : t 𝓝[s] a) :
𝓝[s] a = 𝓝[s t] a
theorem nhds_within_restrict' {α : Type u_1} [topological_space α] {a : α} (s : set α) {t : set α} (h : t 𝓝 a) :
𝓝[s] a = 𝓝[s t] a
theorem nhds_within_restrict {α : Type u_1} [topological_space α] {a : α} (s : set α) {t : set α} (h₀ : a t) (h₁ : is_open t) :
𝓝[s] a = 𝓝[s t] a
theorem nhds_within_le_of_mem {α : Type u_1} [topological_space α] {a : α} {s t : set α} (h : s 𝓝[t] a) :
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 𝓝 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) :
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 𝓝 (π a)) :
π ⁻¹' s 𝓝 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 nhds_within_inter_of_mem {α : Type u_1} [topological_space α] {a : α} {s t : set α} (h : s 𝓝[t] a) :
𝓝[s t] a = 𝓝[t] a
@[simp]
theorem nhds_within_singleton {α : Type u_1} [topological_space α] (a : α) :
𝓝[{a}] a = pure 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 α} :
t 𝓝[insert a s] a a t t 𝓝[s] a
theorem insert_mem_nhds_within_insert {α : Type u_1} [topological_space α] {a : α} {s t : set α} (h : t 𝓝[s] a) :
theorem insert_mem_nhds_iff {α : Type u_1} [topological_space α] {a : α} {s : set α} :
@[simp]
theorem nhds_within_compl_singleton_sup_pure {α : Type u_1} [topological_space α] (a : α) :
theorem nhds_within_prod_eq {α : Type u_1} [topological_space α] {β : Type u_2} [topological_space β] (a : α) (b : β) (s : set α) (t : set β) :
𝓝[s ×ˢ 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 : β} (hu : u 𝓝[s] a) (hv : v 𝓝[t] b) :
u ×ˢ v 𝓝[s ×ˢ t] (a, b)
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) :
𝓝[I.pi s] x = ⨅ (i : ι), filter.comap (λ (x : Π (i : ι), α i), x i) (𝓝 (x i) ⨅ (hi : i I), 𝓟 (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) :
𝓝[I.pi s] x = (⨅ (i : ι) (H : i I), filter.comap (λ (x : Π (i : ι), α i), x i) (𝓝[s i] x i)) ⨅ (i : ι) (H : i I), filter.comap (λ (x : Π (i : ι), α i), x i) (𝓝 (x i))
theorem nhds_within_pi_univ_eq {ι : Type u_1} {α : ι → Type u_2} [fintype ι] [Π (i : ι), topological_space (α i)] (s : Π (i : ι), set (α i)) (x : Π (i : ι), α i) :
𝓝[set.univ.pi s] x = ⨅ (i : ι), filter.comap (λ (x : Π (i : ι), α i), x i) (𝓝[s i] x 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} :
𝓝[I.pi s] x = ∃ (i : ι) (H : i I), 𝓝[s i] x 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} :
(𝓝[I.pi s] x).ne_bot ∀ (i : ι), i I(𝓝[s i] x 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 (𝓝[s t] a) l) (h₁ : filter.tendsto g (𝓝[s t] a) 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 (𝓝[s {x : α | p x}] a) l) (h₁ : filter.tendsto g (𝓝[s {x : α | ¬p x}] a) l) :
filter.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 β} (hst : s t) (h : filter.tendsto f (𝓝[t] a) 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 (𝓝[s] a)) :
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 (𝓝 a) l) :
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 : (𝓝[s] x).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 Ix 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 Idense (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 =ᶠ[𝓝[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 : α} (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 sf x = g x) (hf : filter.tendsto f (𝓝[s] a) l) :
theorem eventually_nhds_within_of_forall {α : Type u_1} [topological_space α] {s : set α} {a : α} {p : α → Prop} (h : ∀ (x : α), x sp x) :
∀ᶠ (x : α) in 𝓝[s] a, 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 (𝓝 a)) (h2 : ∀ᶠ (x : β) in l, f x 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 =ᶠ[𝓝[s] a] 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 𝓝 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 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) :
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.

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) :
filter.tendsto f (𝓝[s] x) (𝓝[f '' s] f 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 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.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_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) :
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 : α} (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 𝓝[s] x) :
theorem continuous_within_at_inter' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s t : set α} {x : α} (h : t 𝓝[s] x) :
theorem continuous_within_at_inter {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s t : set α} {x : α} (h : t 𝓝 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 scontinuous_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 scontinuous_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 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 𝓝 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 𝓝 x) :
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 𝓝 x) :
theorem continuous_at.continuous_on {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} (hcont : ∀ (x : α), x scontinuous_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 𝓝 (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 (𝓝[s] x) = 𝓝[g '' s] g x
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 𝓝[f '' s] f x) :
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 =ᶠ[𝓝[s] x] 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₁ =ᶠ[𝓝[s] x] 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 sf₁ 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 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 β} (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 Tis_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 (𝓝[s] x) = 𝓝[f '' s] f x
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 tfilter.tendsto f (𝓝[s t] a) (𝓝 (t.piecewise f g a))) (hpg : ∀ (a : α), a s frontier tfilter.tendsto g (𝓝[s t] a) (𝓝 (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 (𝓝[s {a : α | p a}] a) (𝓝 (ite (p a) (f a) (g a)))) (hpg : ∀ (a : α), a s frontier {a : α | p a}filter.tendsto g (𝓝[s {a : α | ¬p a}] a) (𝓝 (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 tf 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 (𝓝[{x : α | p x}] a) (𝓝 (ite (p a) (f a) (g a)))) (hpg : ∀ (a : α), a frontier {x : α | p x}filter.tendsto g (𝓝[{x : α | ¬p x}] a) (𝓝 (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 : 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 sf 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 sf 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 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 : α} :