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.
The "neighborhood within" filter. Elements of 𝓝[s] a are sets containing the
intersection of s and a neighborhood of a.
Equations
- nhds_within a s = nhds a ⊓ filter.principal s
@[simp]
theorem
nhds_bind_nhds_within
{α : Type u_1}
[topological_space α]
{a : α}
{s : set α} :
(nhds a).bind (λ (x : α), nhds_within x s) = nhds_within a s
@[simp]
theorem
eventually_nhds_nhds_within
{α : Type u_1}
[topological_space α]
{a : α}
{s : set α}
{p : α → Prop} :
(∀ᶠ (y : α) in nhds a, ∀ᶠ (x : α) in nhds_within y s, p x) ↔ ∀ᶠ (x : α) in nhds_within a s, p x
theorem
eventually_nhds_within_iff
{α : Type u_1}
[topological_space α]
{a : α}
{s : set α}
{p : α → Prop} :
(∀ᶠ (x : α) in nhds_within a s, p x) ↔ ∀ᶠ (x : α) in nhds a, x ∈ s → p x
@[simp]
theorem
eventually_nhds_within_nhds_within
{α : Type u_1}
[topological_space α]
{a : α}
{s : set α}
{p : α → Prop} :
(∀ᶠ (y : α) in nhds_within a s, ∀ᶠ (x : α) in nhds_within y s, p x) ↔ ∀ᶠ (x : α) in nhds_within a s, p x
theorem
nhds_within_eq
{α : Type u_1}
[topological_space α]
(a : α)
(s : set α) :
nhds_within a s = ⨅ (t : set α) (H : t ∈ {t : set α | a ∈ t ∧ is_open t}), filter.principal (t ∩ s)
theorem
nhds_within_univ
{α : Type u_1}
[topological_space α]
(a : α) :
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
mem_nhds_within_iff_exists_mem_nhds_inter
{α : Type u_1}
[topological_space α]
{t : set α}
{a : α}
{s : set α} :
theorem
mem_nhds_within_of_mem_nhds
{α : Type u_1}
[topological_space α]
{s t : set α}
{a : α} :
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
inter_mem_nhds_within
{α : Type u_1}
[topological_space α]
(s : set α)
{t : set α}
{a : α} :
t ∈ nhds a → s ∩ t ∈ nhds_within a s
theorem
nhds_within_mono
{α : Type u_1}
[topological_space α]
(a : α)
{s t : set α} :
s ⊆ t → nhds_within a s ≤ nhds_within a t
theorem
pure_le_nhds_within
{α : Type u_1}
[topological_space α]
{a : α}
{s : set α} :
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 α} :
a ∈ s → t ∈ nhds_within a s → a ∈ t
theorem
filter.eventually.self_of_nhds_within
{α : Type u_1}
[topological_space α]
{p : α → Prop}
{s : set α}
{x : α} :
(∀ᶠ (y : α) in nhds_within x s, p y) → x ∈ s → p x
theorem
tendsto_const_nhds_within
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{l : filter β}
{s : set α}
{a : α} :
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 α} :
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 α} :
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 α} :
a ∈ t → 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 α} :
s ∈ nhds_within a t → nhds_within a t ≤ nhds_within a s
theorem
nhds_within_eq_nhds_within
{α : Type u_1}
[topological_space α]
{a : α}
{s t u : set α} :
a ∈ s → is_open s → t ∩ s = u ∩ s → nhds_within a t = nhds_within a u
theorem
nhds_within_eq_of_open
{α : Type u_1}
[topological_space α]
{a : α}
{s : set α} :
a ∈ s → is_open 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
mem_nhds_within_insert
{α : Type u_1}
[topological_space α]
{a : α}
{s t : set α} :
t ∈ nhds_within a s → has_insert.insert a t ∈ nhds_within a (has_insert.insert a s)
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.prod 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 : β} :
u ∈ nhds_within a s → v ∈ nhds_within b t → u.prod v ∈ nhds_within (a, b) (s.prod t)
theorem
tendsto_if_nhds_within
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{f g : α → β}
{p : α → Prop}
[decidable_pred p]
{a : α}
{s : set α}
{l : filter β} :
filter.tendsto f (nhds_within a (s ∩ p)) l → 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 β} :
s ⊆ t → 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 α} :
s ⊆ t → 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 β} :
filter.tendsto f (nhds a) l → filter.tendsto f (nhds_within a s) l
theorem
principal_subtype
{α : Type u_1}
(s : set α)
(t : set {x // x ∈ s}) :
filter.principal t = filter.comap coe (filter.principal (coe '' t))
theorem
mem_closure_iff_nhds_within_ne_bot
{α : Type u_1}
[topological_space α]
{s : set α}
{x : α} :
x ∈ closure s ↔ (nhds_within x s).ne_bot
theorem
nhds_within_ne_bot_of_mem
{α : Type u_1}
[topological_space α]
{s : set α}
{x : α} :
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 : α} :
(nhds_within x s).ne_bot → x ∈ s
theorem
eventually_eq_nhds_within_iff
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{f g : α → β}
{s : set α}
{a : α} :
theorem
eventually_eq_nhds_within_of_eq_on
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{f g : α → β}
{s : set α}
{a : α} :
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 : α} :
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 β} :
(∀ (x : α), x ∈ s → f x = g x) → filter.tendsto f (nhds_within a s) l → filter.tendsto g (nhds_within a s) l
theorem
eventually_nhds_with_of_forall
{α : Type u_1}
[topological_space α]
{s : set α}
{a : α}
{p : α → Prop} :
(∀ (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}
[topological_space α]
{β : Type u_2}
{a : α}
{l : filter β}
{s : set α}
(f : β → α) :
filter.tendsto f l (nhds a) → (∀ᶠ (x : β) in l, f x ∈ s) → filter.tendsto f l (nhds_within a s)
theorem
filter.eventually_eq.eq_of_nhds_within
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{s : set α}
{f g : α → β}
{a : α} :
f =ᶠ[nhds_within a s] g → a ∈ s → f a = g a
theorem
eventually_nhds_within_of_eventually_nhds
{α : Type u_1}
[topological_space α]
{s : set α}
{a : α}
{p : α → Prop} :
(∀ᶠ (x : α) in nhds a, p x) → (∀ᶠ (x : α) in nhds_within a s, p x)
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 (set.restrict f s) (nhds ⟨a, h⟩) l
def
continuous_within_at
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β] :
(α → β) → set α → α → 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 : α} :
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 β] :
(α → β) → 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 : α} :
continuous_on f s → 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 (set.restrict f s) ⟨x, h⟩
theorem
continuous_within_at.tendsto_nhds_within_image
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{x : α}
{s : set α} :
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 : β} :
continuous_within_at f s x → continuous_within_at g t y → continuous_within_at (prod.map f g) (s.prod t) (x, y)
theorem
continuous_on_iff
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α} :
theorem
continuous_on_iff_continuous_restrict
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α} :
continuous_on f s ↔ continuous (set.restrict f s)
theorem
continuous_on_iff'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α} :
theorem
continuous_on_iff_is_closed
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α} :
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 β} :
continuous_on f s → continuous_on g t → continuous_on (prod.map f g) (s.prod t)
theorem
continuous_on_empty
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : α → β) :
theorem
nhds_within_le_comap
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{x : α}
{s : set α}
{f : α → β} :
continuous_within_at f s x → nhds_within x s ≤ filter.comap f (nhds_within (f x) (f '' s))
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 : α} :
continuous_within_at f t x → s ⊆ t → 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 : α} :
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 : α} :
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 x → 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 : α} :
theorem
continuous_within_at.mem_closure
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α}
{x : α}
{A : set β} :
theorem
continuous_within_at.image_closure
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α} :
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 (set.restrict f s))
{finv : β → α} :
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 : β → α} :
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 α} :
continuous_on f s → set.eq_on g f s₁ → s₁ ⊆ s → continuous_on g s₁
theorem
continuous_on.congr
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f g : α → β}
{s : set α} :
continuous_on f s → 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 α} :
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 : α} :
continuous_at f x → continuous_within_at f s x
theorem
continuous_within_at.continuous_at
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α}
{x : α} :
continuous_within_at f s x → s ∈ nhds x → continuous_at f x
theorem
continuous_on.continuous_at
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α}
{x : α} :
continuous_on f s → s ∈ nhds x → continuous_at f x
theorem
continuous_within_at.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[topological_space α]
[topological_space β]
[topological_space γ]
{g : β → γ}
{f : α → β}
{s : set α}
{t : set β}
{x : α} :
continuous_within_at g t (f x) → continuous_within_at f s x → s ⊆ f ⁻¹' 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 : α} :
continuous_within_at g t (f x) → continuous_within_at f s x → continuous_within_at (g ∘ f) (s ∩ f ⁻¹' t) 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 β} :
continuous_on g t → continuous_on f s → s ⊆ f ⁻¹' t → continuous_on (g ∘ f) s
theorem
continuous_on.mono
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s t : set α} :
continuous_on f s → t ⊆ s → continuous_on f t
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 β} :
continuous_on g t → 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 α} :
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 : α} :
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 α} :
continuous g → 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 β} :
continuous_on g s → continuous f → set.range f ⊆ 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 β} :
continuous_within_at f s x → t ∈ nhds (f x) → f ⁻¹' t ∈ nhds_within x s
theorem
continuous_within_at.preimage_mem_nhds_within'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{x : α}
{s : set α}
{t : set β} :
continuous_within_at f s x → t ∈ nhds_within (f x) (f '' s) → f ⁻¹' t ∈ nhds_within x s
theorem
continuous_within_at.congr_of_eventually_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f f₁ : α → β}
{s : set α}
{x : α} :
continuous_within_at f s x → f₁ =ᶠ[nhds_within x s] f → 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 : α} :
continuous_within_at f s x → (∀ (y : α), y ∈ s → f₁ y = f y) → 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 : α} :
continuous_within_at f s x → set.eq_on g f s₁ → s₁ ⊆ s → 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 α} :
theorem
continuous_on.preimage_open_of_open
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α}
{t : set β} :
theorem
continuous_on.preimage_closed_of_closed
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α}
{t : set β} :
theorem
continuous_on.preimage_interior_subset_interior_preimage
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α}
{t : set β} :
theorem
continuous_on_of_locally_continuous_on
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α} :
(∀ (x : α), x ∈ s → (∃ (t : set α), is_open t ∧ x ∈ t ∧ continuous_on f (s ∩ t))) → continuous_on f s
theorem
continuous_on_open_of_generate_from
{α : Type u_1}
[topological_space α]
{β : Type u_2}
{s : set α}
{T : set (set β)}
{f : α → β} :
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 : α} :
continuous_within_at f s x → 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 α} :
continuous_on f s → continuous_on g s → continuous_on (λ (x : α), (f x, g x)) s
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
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_if'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{s : set α}
{p : α → Prop}
{f g : α → β}
{h : Π (a : α), decidable (p a)} :
(∀ (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)))) → (∀ (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)))) → continuous_on f (s ∩ {a : α | p a}) → 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}
{h : Π (a : α), decidable (p a)}
{s : set α}
{f g : α → β} :
(∀ (a : α), a ∈ s ∩ frontier {a : α | p a} → f a = g a) → continuous_on f (s ∩ closure {a : α | p a}) → continuous_on g (s ∩ closure {a : α | ¬p a}) → continuous_on (λ (a : α), ite (p a) (f a) (g a)) s
theorem
continuous_if'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{p : α → Prop}
{f g : α → β}
{h : Π (a : α), decidable (p a)} :
(∀ (a : α), a ∈ frontier {x : α | p x} → filter.tendsto f (nhds_within a {x : α | p x}) (nhds (ite (p a) (f a) (g a)))) → (∀ (a : α), a ∈ frontier {x : α | p x} → filter.tendsto g (nhds_within a {x : α | ¬p x}) (nhds (ite (p a) (f a) (g a)))) → continuous_on f {x : α | p x} → continuous_on g {x : α | ¬p x} → continuous (λ (a : α), ite (p a) (f a) (g a))
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_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 : α × β} :