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 #
𝓝 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
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_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
@[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_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_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) (nhds x) (nhds (f x))
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