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 #
𝓝 x: the filter of neighborhoods of a pointx;𝓟 s: the principal filter of a sets;𝓝[s] x: the filternhds_within x sof neighborhoods of a pointxwithin a sets.
@[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} :
theorem
mem_closure_ne_iff_frequently_within
{α : Type u_1}
[topological_space α]
{z : α}
{s : set α} :
@[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_univ
{α : Type u_1}
[topological_space α]
(a : α) :
nhds_within a set.univ = nhds 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
diff_mem_nhds_within_compl
{α : Type u_1}
[topological_space α]
{x : α}
{s : set α}
(hs : s ∈ nhds x)
(t : set α) :
s \ t ∈ nhds_within x tᶜ
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) :
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 : α} :
nhds_within x s = nhds_within x t ↔ s =ᶠ[nhds x] t
theorem
nhds_within_le_iff
{α : Type u_1}
[topological_space α]
{s t : set α}
{x : α} :
nhds_within x s ≤ nhds_within x t ↔ t ∈ nhds_within x 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_within a t
theorem
mem_nhds_within_of_mem_nhds
{α : Type u_1}
[topological_space α]
{s t : set α}
{a : α}
(h : s ∈ nhds a) :
s ∈ nhds_within a t
theorem
self_mem_nhds_within
{α : Type u_1}
[topological_space α]
{a : α}
{s : set α} :
s ∈ nhds_within a s
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) :
s ∩ t ∈ nhds_within a s
theorem
nhds_within_mono
{α : Type u_1}
[topological_space α]
(a : α)
{s t : set α}
(h : s ⊆ t) :
nhds_within a s ≤ nhds_within a t
theorem
pure_le_nhds_within
{α : Type u_1}
[topological_space α]
{a : α}
{s : set α}
(ha : a ∈ s) :
has_pure.pure a ≤ nhds_within 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) :
nhds_within a s = nhds_within a (s ∩ t)
theorem
nhds_within_restrict'
{α : Type u_1}
[topological_space α]
{a : α}
(s : set α)
{t : set α}
(h : t ∈ nhds a) :
nhds_within a s = nhds_within a (s ∩ t)
theorem
nhds_within_restrict
{α : Type u_1}
[topological_space α]
{a : α}
(s : set α)
{t : set α}
(h₀ : a ∈ t)
(h₁ : is_open t) :
nhds_within a s = nhds_within a (s ∩ t)
theorem
nhds_within_le_of_mem
{α : Type u_1}
[topological_space α]
{a : α}
{s t : set α}
(h : s ∈ nhds_within a t) :
nhds_within a t ≤ nhds_within a s
theorem
nhds_within_le_nhds
{α : Type u_1}
[topological_space α]
{a : α}
{s : set α} :
nhds_within a s ≤ nhds a
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) :
nhds_within a t = nhds_within a u
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) :
nhds_within a t = nhds_within a u
@[simp]
theorem
is_open.nhds_within_eq
{α : Type u_1}
[topological_space α]
{a : α}
{s : set α}
(h : is_open s)
(ha : a ∈ s) :
nhds_within a s = nhds a
@[simp]
theorem
nhds_within_union
{α : Type u_1}
[topological_space α]
(a : α)
(s t : set α) :
nhds_within a (s ∪ t) = nhds_within a s ⊔ nhds_within a t
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 α) :
nhds_within a (s ∩ t) = nhds_within a s ⊓ nhds_within a t
theorem
nhds_within_inter'
{α : Type u_1}
[topological_space α]
(a : α)
(s t : set α) :
nhds_within a (s ∩ t) = nhds_within a s ⊓ filter.principal t
theorem
nhds_within_inter_of_mem
{α : Type u_1}
[topological_space α]
{a : α}
{s t : set α}
(h : s ∈ nhds_within a t) :
nhds_within a (s ∩ t) = 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) :
nhds_within a (t ∩ s) = nhds_within a t
@[simp]
theorem
nhds_within_singleton
{α : Type u_1}
[topological_space α]
(a : α) :
nhds_within a {a} = has_pure.pure a
@[simp]
theorem
nhds_within_insert
{α : Type u_1}
[topological_space α]
(a : α)
(s : set α) :
nhds_within a (has_insert.insert a s) = has_pure.pure a ⊔ nhds_within a s
theorem
mem_nhds_within_insert
{α : Type u_1}
[topological_space α]
{a : α}
{s t : set α} :
t ∈ nhds_within a (has_insert.insert a s) ↔ a ∈ t ∧ t ∈ nhds_within a s
theorem
insert_mem_nhds_within_insert
{α : Type u_1}
[topological_space α]
{a : α}
{s t : set α}
(h : t ∈ nhds_within a s) :
has_insert.insert a t ∈ nhds_within a (has_insert.insert a s)
theorem
insert_mem_nhds_iff
{α : Type u_1}
[topological_space α]
{a : α}
{s : set α} :
has_insert.insert a s ∈ nhds a ↔ s ∈ nhds_within a {a}ᶜ
@[simp]
theorem
nhds_within_compl_singleton_sup_pure
{α : Type u_1}
[topological_space α]
(a : α) :
nhds_within a {a}ᶜ ⊔ has_pure.pure a = nhds a
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_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) :
filter.tendsto (t.piecewise f g) (nhds_within a s) 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) :
filter.tendsto f (nhds_within a s) 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)) :
filter.tendsto f l (nhds_within a t)
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) :
filter.tendsto f (nhds_within a s) 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)) :
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)) :
filter.tendsto f l (nhds a)
theorem
principal_subtype
{α : Type u_1}
(s : set α)
(t : set {x // x ∈ s}) :
filter.principal t = filter.comap coe (filter.principal (coe '' t))
theorem
nhds_within_ne_bot_of_mem
{α : Type u_1}
[topological_space α]
{s : set α}
{x : α}
(hx : x ∈ s) :
(nhds_within x s).ne_bot
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 : α) :
(nhds_within x (set.range f)).ne_bot
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 =ᶠ[nhds_within a s] g
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 =ᶠ[nhds_within a s] g
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) :
filter.tendsto g (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) :
filter.tendsto f l (nhds_within a 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 : β → α} :
filter.tendsto f l (nhds_within a (set.range f)) ↔ filter.tendsto f l (nhds a)
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}} :
t ∈ nhds_within a u ↔ t ∈ filter.comap coe (nhds_within ↑a (coe '' u))
theorem
nhds_within_subtype
{α : Type u_1}
[topological_space α]
(s : set α)
(a : {x // x ∈ s})
(t : set {x // x ∈ s}) :
nhds_within a t = filter.comap coe (nhds_within ↑a (coe '' t))
theorem
nhds_within_eq_map_subtype_coe
{α : Type u_1}
[topological_space α]
{s : set α}
{a : α}
(h : a ∈ s) :
nhds_within a s = filter.map coe (nhds ⟨a, h⟩)
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 (nhds_within a s) l ↔ filter.tendsto (s.restrict f) (nhds ⟨a, h⟩) l
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
- continuous_within_at f s x = filter.tendsto f (nhds_within x s) (nhds (f x))
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 (nhds_within x s) (nhds (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
- continuous_on f s = ∀ (x : α), x ∈ s → continuous_within_at f s x
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
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
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⟩
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 (nhds_within x s) (nhds_within (f x) 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 (nhds_within x s) (nhds_within (f x) (f '' s))
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)
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_continuous_restrict
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α} :
continuous_on f s ↔ continuous (s.restrict f)
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.
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.
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)
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 : α) :
continuous_on f {a}
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
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) :
nhds_within x s ≤ filter.comap f (nhds_within (f x) (f '' s))
@[simp]
theorem
comap_nhds_within_range
{β : Type u_2}
[topological_space β]
{α : Type u_1}
(f : α → β)
(y : β) :
filter.comap f (nhds_within y (set.range f)) = filter.comap f (nhds y)
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) :
continuous_within_at f s x
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) :
continuous_within_at f s x
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) :
continuous_within_at f (s ∩ t) x ↔ continuous_within_at f s x
theorem
continuous_within_at_inter
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s t : set α}
{x : α}
(h : t ∈ nhds x) :
continuous_within_at f (s ∩ t) x ↔ continuous_within_at f s x
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
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
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) :
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) :
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)
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)
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) :
theorem
continuous_on.image_closure
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α}
(hf : continuous_on f (closure s)) :
@[simp]
theorem
continuous_within_at_singleton
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{x : α} :
continuous_within_at f {x} x
@[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 (has_insert.insert x s) x ↔ continuous_within_at f s x
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 (has_insert.insert x s) x
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) :
continuous_within_at f (s \ t) x ↔ continuous_within_at f s x
@[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
@[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
@[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 (nhds_within x (s \ {x})) (nhds y)
@[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 (nhds_within x {x}ᶜ) (nhds 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) :
continuous_on finv (set.range 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) :
continuous_on g 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) :
continuous_on g 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) :
continuous_on g s ↔ continuous_on 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) :
continuous_within_at f s 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) :
continuous_within_at f s x ↔ continuous_at f 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) :
continuous_at f 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) :
continuous_at f 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) :
continuous_on f s
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
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
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
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
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
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) :
continuous_on f s
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
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
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)
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)) :
f ⁻¹' t ∈ nhds_within x s
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) :
filter.map g (nhds x) = nhds_within (g x) (set.range g)
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)) :
f ⁻¹' t ∈ nhds_within x 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) :
continuous_within_at f s x ↔ continuous_within_at g s x
theorem
continuous_within_at.congr_of_eventually_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f f₁ : α → β}
{s : set α}
{x : α}
(h : continuous_within_at f s x)
(h₁ : f₁ =ᶠ[nhds_within x s] f)
(hx : f₁ x = f x) :
continuous_within_at f₁ s x
theorem
continuous_within_at.congr
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f f₁ : α → β}
{s : set α}
{x : α}
(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
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
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_open_iff
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α}
(hs : is_open s) :
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))) :
continuous_on f s
theorem
continuous_within_at.prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α → β}
{g : α → γ}
{s : set α}
{x : α}
(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 : α} :
continuous_within_at f s x ↔ continuous_within_at (g ∘ f) s 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 α} :
continuous_on f s ↔ continuous_on (g ∘ f) s
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
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 : α) :
filter.map f (nhds_within x (f ⁻¹' s)) = nhds_within (f x) s
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
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ᶜ)) :
continuous_on (t.piecewise f g) s
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ᶜ)) :
continuous_on (t.piecewise f g) s
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ᶜ)) :
continuous (s.piecewise f g)
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)
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 : α} :
continuous_within_at f s x ↔ continuous_within_at (prod.fst ∘ f) s x ∧ continuous_within_at (prod.snd ∘ f) s x