mathlib documentation

topology.continuous_on

Neighborhoods and continuity relative to a subset #

This file defines relative versions

and proves their basic properties, including the relationships between these restricted notions and the corresponding notions for the subtype equipped with the subspace topology.

Notation #

source
@[simp]
theorem nhds_bind_nhds_within {α : Type u_1} [topological_space α] {a : α} {s : set α} :
(𝓝 a).bind (λ (x : α), 𝓝[s] x) = 𝓝[s] a
source
@[simp]
theorem eventually_nhds_nhds_within {α : Type u_1} [topological_space α] {a : α} {s : set α} {p : α → Prop} :
(∀ᶠ (y : α) in 𝓝 a, ∀ᶠ (x : α) in 𝓝[s] y, p x) ↔ ∀ᶠ (x : α) in 𝓝[s] a, p x
source
theorem eventually_nhds_within_iff {α : Type u_1} [topological_space α] {a : α} {s : set α} {p : α → Prop} :
(∀ᶠ (x : α) in 𝓝[s] a, p x) ↔ ∀ᶠ (x : α) in 𝓝 a, x ∈ s → p x
source
@[simp]
theorem eventually_nhds_within_nhds_within {α : Type u_1} [topological_space α] {a : α} {s : set α} {p : α → Prop} :
(∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x) ↔ ∀ᶠ (x : α) in 𝓝[s] a, p x
source
theorem nhds_within_eq {α : Type u_1} [topological_space α] (a : α) (s : set α) :
𝓝[s] a = ⨅ (t : set α) (H : t ∈ {t : set α | a ∈ t ∧ is_open t}), 𝓟 (t ∩ s)
source
theorem nhds_within_univ {α : Type u_1} [topological_space α] (a : α) :
𝓝[set.univ] a = 𝓝 a
source
theorem nhds_within_has_basis {α : Type u_1} {β : Type u_2} [topological_space α] {p : β → Prop} {s : β → set α} {a : α} (h : (𝓝 a).has_basis p s) (t : set α) :
(𝓝[t] a).has_basis p (λ (i : β), s i ∩ t)
source
theorem nhds_within_basis_open {α : Type u_1} [topological_space α] (a : α) (t : set α) :
(𝓝[t] a).has_basis (λ (u : set α), a ∈ u ∧ is_open u) (λ (u : set α), u ∩ t)
source
theorem mem_nhds_within {α : Type u_1} [topological_space α] {t : set α} {a : α} {s : set α} :
t ∈ 𝓝[s] a ↔ ∃ (u : set α), is_open u ∧ a ∈ u ∧ u ∩ s ⊆ t
source
theorem mem_nhds_within_iff_exists_mem_nhds_inter {α : Type u_1} [topological_space α] {t : set α} {a : α} {s : set α} :
t ∈ 𝓝[s] a ↔ ∃ (u : set α) (H : u ∈ 𝓝 a), u ∩ s ⊆ t
source
theorem diff_mem_nhds_within_compl {α : Type u_1} [topological_space α] {x : α} {s : set α} (hs : s ∈ 𝓝 x) (t : set α) :
s \ t ∈ 𝓝[tᶜ] x
source
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
source
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
source
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
source
theorem mem_nhds_within_of_mem_nhds {α : Type u_1} [topological_space α] {s t : set α} {a : α} (h : s ∈ 𝓝 a) :
s ∈ 𝓝[t] a
source
theorem self_mem_nhds_within {α : Type u_1} [topological_space α] {a : α} {s : set α} :
s ∈ 𝓝[s] a
source
theorem inter_mem_nhds_within {α : Type u_1} [topological_space α] (s : set α) {t : set α} {a : α} (h : t ∈ 𝓝 a) :
s ∩ t ∈ 𝓝[s] a
source
theorem nhds_within_mono {α : Type u_1} [topological_space α] (a : α) {s t : set α} (h : s ⊆ t) :
𝓝[s] a ≤ 𝓝[t] a
source
theorem pure_le_nhds_within {α : Type u_1} [topological_space α] {a : α} {s : set α} (ha : a ∈ s) :
pure a ≤ 𝓝[s] a
source
theorem mem_of_mem_nhds_within {α : Type u_1} [topological_space α] {a : α} {s t : set α} (ha : a ∈ s) (ht : t ∈ 𝓝[s] a) :
a ∈ t
source
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
source
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)
source
theorem nhds_within_restrict'' {α : Type u_1} [topological_space α] {a : α} (s : set α) {t : set α} (h : t ∈ 𝓝[s] a) :
𝓝[s] a = 𝓝[s ∩ t] a
source
theorem nhds_within_restrict' {α : Type u_1} [topological_space α] {a : α} (s : set α) {t : set α} (h : t ∈ 𝓝 a) :
𝓝[s] a = 𝓝[s ∩ t] a
source
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
source
theorem nhds_within_le_of_mem {α : Type u_1} [topological_space α] {a : α} {s t : set α} (h : s ∈ 𝓝[t] a) :
𝓝[t] a ≤ 𝓝[s] a
source
theorem nhds_within_le_nhds {α : Type u_1} [topological_space α] {a : α} {s : set α} :
𝓝[s] a ≤ 𝓝 a
source
theorem nhds_within_eq_nhds_within' {α : Type u_1} [topological_space α] {a : α} {s t u : set α} (hs : s ∈ 𝓝 a) (h₂ : t ∩ s = u ∩ s) :
𝓝[t] a = 𝓝[u] a
source
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) :
𝓝[t] a = 𝓝[u] a
source
theorem is_open.nhds_within_eq {α : Type u_1} [topological_space α] {a : α} {s : set α} (h : is_open s) (ha : a ∈ s) :
𝓝[s] a = 𝓝 a
source
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
source
@[simp]
theorem nhds_within_empty {α : Type u_1} [topological_space α] (a : α) :
𝓝[∅] a = ⊥
source
theorem nhds_within_union {α : Type u_1} [topological_space α] (a : α) (s t : set α) :
𝓝[s ∪ t] a = 𝓝[s] a ⊔ 𝓝[t] a
source
theorem nhds_within_inter {α : Type u_1} [topological_space α] (a : α) (s t : set α) :
𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓝[t] a
source
theorem nhds_within_inter' {α : Type u_1} [topological_space α] (a : α) (s t : set α) :
𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓟 t
source
theorem nhds_within_inter_of_mem {α : Type u_1} [topological_space α] {a : α} {s t : set α} (h : s ∈ 𝓝[t] a) :
𝓝[s ∩ t] a = 𝓝[t] a
source
@[simp]
theorem nhds_within_singleton {α : Type u_1} [topological_space α] (a : α) :
𝓝[{a}] a = pure a
source
@[simp]
theorem nhds_within_insert {α : Type u_1} [topological_space α] (a : α) (s : set α) :
𝓝[insert a s] a = pure a ⊔ 𝓝[s] a
source
theorem mem_nhds_within_insert {α : Type u_1} [topological_space α] {a : α} {s t : set α} :
t ∈ 𝓝[insert a s] a ↔ a ∈ t ∧ t ∈ 𝓝[s] a
source
theorem insert_mem_nhds_within_insert {α : Type u_1} [topological_space α] {a : α} {s t : set α} (h : t ∈ 𝓝[s] a) :
insert a t ∈ 𝓝[insert a s] a
source
theorem insert_mem_nhds_iff {α : Type u_1} [topological_space α] {a : α} {s : set α} :
insert a s ∈ 𝓝 a ↔ s ∈ 𝓝[{a}ᶜ] a
source
@[simp]
theorem nhds_within_compl_singleton_sup_pure {α : Type u_1} [topological_space α] (a : α) :
𝓝[{a}ᶜ] a ⊔ pure a = 𝓝 a
source
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
source
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)
source
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))
source
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))
source
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)
source
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 = ⊥
source
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
source
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) :
filter.tendsto (t.piecewise f g) (𝓝[s] a) l
source
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
source
theorem map_nhds_within {α : Type u_1} {β : Type u_2} [topological_space α] (f : α → β) (a : α) (s : set α) :
filter.map f (𝓝[s] a) = ⨅ (t : set α) (H : t ∈ {t : set α | a ∈ t ∧ is_open t}), 𝓟 (f '' (t ∩ s))
source
theorem tendsto_nhds_within_mono_left {α : Type u_1} {β : Type u_2} [topological_space α] {f : α → β} {a : α} {s t : set α} {l : filter β} (hst : s ⊆ t) (h : filter.tendsto f (𝓝[t] a) l) :
filter.tendsto f (𝓝[s] a) l
source
theorem tendsto_nhds_within_mono_right {α : Type u_1} {β : Type u_2} [topological_space α] {f : β → α} {l : filter β} {a : α} {s t : set α} (hst : s ⊆ t) (h : filter.tendsto f l (𝓝[s] a)) :
filter.tendsto f l (𝓝[t] a)
source
theorem tendsto_nhds_within_of_tendsto_nhds {α : Type u_1} {β : Type u_2} [topological_space α] {f : α → β} {a : α} {s : set α} {l : filter β} (h : filter.tendsto f (𝓝 a) l) :
filter.tendsto f (𝓝[s] a) l
source
theorem principal_subtype {α : Type u_1} (s : set α) (t : set {x // x ∈ s}) :
𝓟 t = filter.comap coe (𝓟 (coe '' t))
source
theorem nhds_within_ne_bot_of_mem {α : Type u_1} [topological_space α] {s : set α} {x : α} (hx : x ∈ s) :
(𝓝[s] x).ne_bot
source
theorem is_closed.mem_of_nhds_within_ne_bot {α : Type u_1} [topological_space α] {s : set α} (hs : is_closed s) {x : α} (hx : (𝓝[s] x).ne_bot) :
x ∈ s
source
theorem dense_range.nhds_within_ne_bot {α : Type u_1} [topological_space α] {ι : Type u_2} {f : ι → α} (h : dense_range f) (x : α) :
(𝓝[set.range f] x).ne_bot
source
theorem 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)
source
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))
source
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)
source
theorem eventually_eq_nhds_within_iff {α : Type u_1} {β : Type u_2} [topological_space α] {f g : α → β} {s : set α} {a : α} :
f =ᶠ[𝓝[s] a] g ↔ ∀ᶠ (x : α) in 𝓝 a, x ∈ s → f x = g x
source
theorem eventually_eq_nhds_within_of_eq_on {α : Type u_1} {β : Type u_2} [topological_space α] {f g : α → β} {s : set α} {a : α} (h : set.eq_on f g s) :
f =ᶠ[𝓝[s] a] g
source
theorem set.eq_on.eventually_eq_nhds_within {α : Type u_1} {β : Type u_2} [topological_space α] {f g : α → β} {s : set α} {a : α} (h : set.eq_on f g s) :
f =ᶠ[𝓝[s] a] g
source
theorem tendsto_nhds_within_congr {α : Type u_1} {β : Type u_2} [topological_space α] {f g : α → β} {s : set α} {a : α} {l : filter β} (hfg : ∀ (x : α), x ∈ s → f x = g x) (hf : filter.tendsto f (𝓝[s] a) l) :
filter.tendsto g (𝓝[s] a) l
source
theorem eventually_nhds_within_of_forall {α : Type u_1} [topological_space α] {s : set α} {a : α} {p : α → Prop} (h : ∀ (x : α), x ∈ s → p x) :
∀ᶠ (x : α) in 𝓝[s] a, p x
source
theorem tendsto_nhds_within_of_tendsto_nhds_of_eventually_within {α : Type u_1} {β : Type u_2} [topological_space α] {a : α} {l : filter β} {s : set α} (f : β → α) (h1 : filter.tendsto f l (𝓝 a)) (h2 : ∀ᶠ (x : β) in l, f x ∈ s) :
filter.tendsto f l (𝓝[s] a)
source
@[simp]
theorem tendsto_nhds_within_range {α : Type u_1} {β : Type u_2} [topological_space α] {a : α} {l : filter β} {f : β → α} :
filter.tendsto f l (𝓝[set.range f] a) ↔ filter.tendsto f l (𝓝 a)
source
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
source
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 #

source
theorem mem_nhds_within_subtype {α : Type u_1} [topological_space α] {s : set α} {a : {x // x ∈ s}} {t u : set {x // x ∈ s}} :
t ∈ 𝓝[u] a ↔ t ∈ filter.comap coe (𝓝[coe '' u] ↑a)
source
theorem nhds_within_subtype {α : Type u_1} [topological_space α] (s : set α) (a : {x // x ∈ s}) (t : set {x // x ∈ s}) :
𝓝[t] a = filter.comap coe (𝓝[coe '' t] ↑a)
source
theorem nhds_within_eq_map_subtype_coe {α : Type u_1} [topological_space α] {s : set α} {a : α} (h : a ∈ s) :
𝓝[s] a = filter.map coe (𝓝 ⟨a, h⟩)
source
theorem mem_nhds_subtype_iff_nhds_within {α : Type u_1} [topological_space α] {s : set α} {a : ↥s} {t : set ↥s} :
t ∈ 𝓝 a ↔ coe '' t ∈ 𝓝[s] ↑a
source
theorem preimage_coe_mem_nhds_subtype {α : Type u_1} [topological_space α] {s t : set α} {a : ↥s} :
coe ⁻¹' t ∈ 𝓝 a ↔ t ∈ 𝓝[s] ↑a
source
theorem tendsto_nhds_within_iff_subtype {α : Type u_1} {β : Type u_2} [topological_space α] {s : set α} {a : α} (h : a ∈ s) (f : α → β) (l : filter β) :
filter.tendsto f (𝓝[s] a) l ↔ filter.tendsto (s.restrict f) (𝓝 ⟨a, h⟩) l
source
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
source
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.

source
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
source
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) :
continuous_within_at f s x
source
theorem continuous_within_at_univ {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) (x : α) :
continuous_within_at f set.univ x ↔ continuous_at f x
source
theorem continuous_within_at_iff_continuous_at_restrict {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) {x : α} {s : set α} (h : x ∈ s) :
continuous_within_at f s x ↔ continuous_at (s.restrict f) ⟨x, h⟩
source
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) :
filter.tendsto f (𝓝[s] x) (𝓝[t] f x)
source
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)
source
theorem continuous_within_at.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {f : α → γ} {g : β → δ} {s : set α} {t : set β} {x : α} {y : β} (hf : continuous_within_at f s x) (hg : continuous_within_at g t y) :
continuous_within_at (prod.map f g) (s ×ˢ t) (x, y)
source
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
source
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
source
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
source
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
source
theorem continuous_on_iff {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} :
continuous_on f s ↔ ∀ (x : α), x ∈ s → ∀ (t : set β), is_open t → f x ∈ t → (∃ (u : set α), is_open u ∧ x ∈ u ∧ u ∩ s ⊆ f ⁻¹' t)
source
theorem continuous_on_iff_continuous_restrict {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} :
continuous_on f s ↔ continuous (s.restrict f)
source
theorem continuous_on_iff' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} :
continuous_on f s ↔ ∀ (t : set β), is_open t → (∃ (u : set α), is_open u ∧ f ⁻¹' t ∩ s = u ∩ s)
source
theorem continuous_on.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) :
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.

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

source
theorem continuous_on_iff_is_closed {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} :
continuous_on f s ↔ ∀ (t : set β), is_closed t → (∃ (u : set α), is_closed u ∧ f ⁻¹' t ∩ s = u ∩ s)
source
theorem continuous_on.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {f : α → γ} {g : β → δ} {s : set α} {t : set β} (hf : continuous_on f s) (hg : continuous_on g t) :
continuous_on (prod.map f g) (s ×ˢ t)
source
theorem continuous_on_empty {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) :
continuous_on f ∅
source
theorem continuous_on_singleton {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) (a : α) :
continuous_on f {a}
source
theorem set.subsingleton.continuous_on {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set α} (hs : s.subsingleton) (f : α → β) :
continuous_on f s
source
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) :
𝓝[s] x ≤ filter.comap f (𝓝[f '' s] f x)
source
theorem continuous_within_at_iff_ptendsto_res {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) {x : α} {s : set α} :
continuous_within_at f s x ↔ filter.ptendsto (pfun.res f s) (𝓝 x) (𝓝 (f x))
source
theorem continuous_iff_continuous_on_univ {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :
continuous f ↔ continuous_on f set.univ
source
theorem continuous_within_at.mono {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s t : set α} {x : α} (h : continuous_within_at f t x) (hs : s ⊆ t) :
continuous_within_at f s x
source
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) :
continuous_within_at f s x
source
theorem continuous_within_at_inter' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s t : set α} {x : α} (h : t ∈ 𝓝[s] x) :
continuous_within_at f (s ∩ t) x ↔ continuous_within_at f s x
source
theorem continuous_within_at_inter {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s t : set α} {x : α} (h : t ∈ 𝓝 x) :
continuous_within_at f (s ∩ t) x ↔ continuous_within_at f s x
source
theorem continuous_within_at_union {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s t : set α} {x : α} :
continuous_within_at f (s ∪ t) x ↔ continuous_within_at f s x ∧ continuous_within_at f t x
source
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) :
continuous_within_at f (s ∪ t) x
source
theorem continuous_within_at.mem_closure_image {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {x : α} (h : continuous_within_at f s x) (hx : x ∈ closure s) :
f x ∈ closure (f '' s)
source
theorem continuous_within_at.mem_closure {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {x : α} {A : set β} (h : continuous_within_at f s x) (hx : x ∈ closure s) (hA : set.maps_to f s A) :
f x ∈ closure A
source
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) :
set.maps_to f (closure s) (closure t)
source
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)) :
set.maps_to f (closure s) (closure t)
source
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)
source
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)
source
@[simp]
theorem continuous_within_at_singleton {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} :
continuous_within_at f {x} x
source
@[simp]
theorem continuous_within_at_insert_self {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} {s : set α} :
continuous_within_at f (insert x s) x ↔ continuous_within_at f s x
source
theorem continuous_within_at.insert_self {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} {s : set α} :
continuous_within_at f s x → continuous_within_at f (insert x s) x

Alias of continuous_within_at_insert_self.

source
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) :
continuous_within_at f (s \ t) x ↔ continuous_within_at f s x
source
@[simp]
theorem continuous_within_at_diff_self {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {x : α} :
continuous_within_at f (s \ {x}) x ↔ continuous_within_at f s x
source
@[simp]
theorem continuous_within_at_compl_self {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {a : α} :
continuous_within_at f {a}ᶜ a ↔ continuous_at f a
source
@[simp]
theorem continuous_within_at_update_same {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [decidable_eq α] {f : α → β} {s : set α} {x : α} {y : β} :
continuous_within_at (function.update f x y) s x ↔ filter.tendsto f (𝓝[s \ {x}] x) (𝓝 y)
source
@[simp]
theorem continuous_at_update_same {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [decidable_eq α] {f : α → β} {x : α} {y : β} :
continuous_at (function.update f x y) x ↔ filter.tendsto f (𝓝[{x}ᶜ] x) (𝓝 y)
source
theorem is_open_map.continuous_on_image_of_left_inv_on {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} (h : is_open_map (s.restrict f)) {finv : β → α} (hleft : set.left_inv_on finv f s) :
continuous_on finv (f '' s)
source
theorem is_open_map.continuous_on_range_of_left_inverse {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : is_open_map f) {finv : β → α} (hleft : function.left_inverse finv f) :
continuous_on finv (set.range f)
source
theorem continuous_on.congr_mono {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : α → β} {s s₁ : set α} (h : continuous_on f s) (h' : set.eq_on g f s₁) (h₁ : s₁ ⊆ s) :
continuous_on g s₁
source
theorem continuous_on.congr {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : α → β} {s : set α} (h : continuous_on f s) (h' : set.eq_on g f s) :
continuous_on g s
source
theorem continuous_on_congr {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : α → β} {s : set α} (h' : set.eq_on g f s) :
continuous_on g s ↔ continuous_on f s
source
theorem continuous_at.continuous_within_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {x : α} (h : continuous_at f x) :
continuous_within_at f s x
source
theorem continuous_within_at_iff_continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {x : α} (h : s ∈ 𝓝 x) :
continuous_within_at f s x ↔ continuous_at f x
source
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) :
continuous_at f x
source
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) :
continuous_at f x
source
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) :
continuous_on f s
source
theorem continuous_within_at.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} {s : set α} {t : set β} {x : α} (hg : continuous_within_at g t (f x)) (hf : continuous_within_at f s x) (h : set.maps_to f s t) :
continuous_within_at (g ∘ f) s x
source
theorem continuous_within_at.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} {s : set α} {t : set β} {x : α} (hg : continuous_within_at g t (f x)) (hf : continuous_within_at f s x) :
continuous_within_at (g ∘ f) (s ∩ f ⁻¹' t) x
source
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) :
continuous_within_at (g ∘ f) s x
source
theorem continuous_on.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} {s : set α} {t : set β} (hg : continuous_on g t) (hf : continuous_on f s) (h : set.maps_to f s t) :
continuous_on (g ∘ f) s
source
theorem continuous_on.mono {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s t : set α} (hf : continuous_on f s) (h : t ⊆ s) :
continuous_on f t
source
theorem antitone_continuous_on {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :
antitone (continuous_on f)
source
theorem continuous_on.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} {s : set α} {t : set β} (hg : continuous_on g t) (hf : continuous_on f s) :
continuous_on (g ∘ f) (s ∩ f ⁻¹' t)
source
theorem continuous.continuous_on {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} (h : continuous f) :
continuous_on f s
source
theorem continuous.continuous_within_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {x : α} (h : continuous f) :
continuous_within_at f s x
source
theorem continuous.comp_continuous_on {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} {s : set α} (hg : continuous g) (hf : continuous_on f s) :
continuous_on (g ∘ f) s
source
theorem continuous_on.comp_continuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} {s : set β} (hg : continuous_on g s) (hf : continuous f) (hs : ∀ (x : α), f x ∈ s) :
continuous (g ∘ f)
source
theorem continuous_within_at.preimage_mem_nhds_within {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} {s : set α} {t : set β} (h : continuous_within_at f s x) (ht : t ∈ 𝓝 (f x)) :
f ⁻¹' t ∈ 𝓝[s] x
source
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
source
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) :
filter.map g (𝓝 x) = 𝓝[set.range g] g x
source
theorem continuous_within_at.preimage_mem_nhds_within' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} {s : set α} {t : set β} (h : continuous_within_at f s x) (ht : t ∈ 𝓝[f '' s] f x) :
f ⁻¹' t ∈ 𝓝[s] x
source
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) :
continuous_within_at f s x ↔ continuous_within_at g s x
source
theorem continuous_within_at.congr_of_eventually_eq {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f f₁ : α → β} {s : set α} {x : α} (h : continuous_within_at f s x) (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
continuous_within_at f₁ s x
source
theorem continuous_within_at.congr {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f f₁ : α → β} {s : set α} {x : α} (h : continuous_within_at f s x) (h₁ : ∀ (y : α), y ∈ s → f₁ y = f y) (hx : f₁ x = f x) :
continuous_within_at f₁ s x
source
theorem continuous_within_at.congr_mono {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : α → β} {s s₁ : set α} {x : α} (h : continuous_within_at f s x) (h' : set.eq_on g f s₁) (h₁ : s₁ ⊆ s) (hx : g x = f x) :
continuous_within_at g s₁ x
source
theorem continuous_on_const {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set α} {c : β} :
continuous_on (λ (x : α), c) s
source
theorem continuous_within_at_const {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {b : β} {s : set α} {x : α} :
continuous_within_at (λ (_x : α), b) s x
source
theorem continuous_on_id {α : Type u_1} [topological_space α] {s : set α} :
continuous_on id s
source
theorem continuous_within_at_id {α : Type u_1} [topological_space α] {s : set α} {x : α} :
continuous_within_at id s x
source
theorem continuous_on_open_iff {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} (hs : is_open s) :
continuous_on f s ↔ ∀ (t : set β), is_open t → is_open (s ∩ f ⁻¹' t)
source
theorem continuous_on.preimage_open_of_open {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {t : set β} (hf : continuous_on f s) (hs : is_open s) (ht : is_open t) :
is_open (s ∩ f ⁻¹' t)
source
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) :
is_open (f ⁻¹' t)
source
theorem continuous_on.preimage_closed_of_closed {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {t : set β} (hf : continuous_on f s) (hs : is_closed s) (ht : is_closed t) :
is_closed (s ∩ f ⁻¹' t)
source
theorem continuous_on.preimage_interior_subset_interior_preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {t : set β} (hf : continuous_on f s) (hs : is_open s) :
s ∩ f ⁻¹' interior t ⊆ s ∩ interior (f ⁻¹' t)
source
theorem continuous_on_of_locally_continuous_on {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} (h : ∀ (x : α), x ∈ s → (∃ (t : set α), is_open t ∧ x ∈ t ∧ continuous_on f (s ∩ t))) :
continuous_on f s
source
theorem continuous_on_open_of_generate_from {α : Type u_1} [topological_space α] {β : Type u_2} {s : set α} {T : set (set β)} {f : α → β} (hs : is_open s) (h : ∀ (t : set β), t ∈ T → is_open (s ∩ f ⁻¹' t)) :
continuous_on f s
source
theorem continuous_within_at.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α → β} {g : α → γ} {s : set α} {x : α} (hf : continuous_within_at f s x) (hg : continuous_within_at g s x) :
continuous_within_at (λ (x : α), (f x, g x)) s x
source
theorem continuous_on.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α → β} {g : α → γ} {s : set α} (hf : continuous_on f s) (hg : continuous_on g s) :
continuous_on (λ (x : α), (f x, g x)) s
source
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 : α} :
continuous_within_at f s x ↔ continuous_within_at (g ∘ f) s x
source
theorem inducing.continuous_on_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α → β} {g : β → γ} (hg : inducing g) {s : set α} :
continuous_on f s ↔ continuous_on (g ∘ f) s
source
theorem embedding.continuous_on_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {f : α → β} {g : β → γ} (hg : embedding g) {s : set α} :
continuous_on f s ↔ continuous_on (g ∘ f) s
source
theorem 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
source
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 : α) :
filter.map f (𝓝[f ⁻¹' s] x) = 𝓝[s] f x
source
theorem continuous_within_at_of_not_mem_closure {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} {x : α} :
x ∉ closure s → continuous_within_at f s x
source
theorem continuous_on.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 (𝓝[s ∩ t] a) (𝓝 (t.piecewise f g a))) (hpg : ∀ (a : α), a ∈ s ∩ frontier t → filter.tendsto g (𝓝[s ∩ tᶜ] a) (𝓝 (t.piecewise f g a))) (hf : continuous_on f (s ∩ t)) (hg : continuous_on g (s ∩ tᶜ)) :
continuous_on (t.piecewise f g) s
source
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
source
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
source
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ᶜ)) :
continuous_on (t.piecewise f g) s
source
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))
source
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))
source
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))
source
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))
source
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ᶜ)) :
continuous (s.piecewise f g)
source
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) :
continuous (s.piecewise f g)
source
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')
source
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')
source
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
source
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) :
t.ite s s' ∩ closure tᶜ = s' ∩ closure tᶜ
source
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')
source
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')
source
theorem continuous_on_fst {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set (α × β)} :
continuous_on prod.fst s
source
theorem continuous_within_at_fst {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set (α × β)} {p : α × β} :
continuous_within_at prod.fst s p
source
theorem continuous_on.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
source
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
source
theorem continuous_on_snd {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set (α × β)} :
continuous_on prod.snd s
source
theorem continuous_within_at_snd {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set (α × β)} {p : α × β} :
continuous_within_at prod.snd s p
source
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
source
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
source
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 : α} :
continuous_within_at f s x ↔ continuous_within_at (prod.fst ∘ f) s x ∧ continuous_within_at (prod.snd ∘ f) s x