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
eventually_nhds_nhds_within
{α : Type u_1}
[topological_space α]
{a : α}
{s : set α}
{p : α → Prop} :
theorem
eventually_nhds_within_iff
{α : Type u_1}
[topological_space α]
{a : α}
{s : set α}
{p : α → Prop} :
theorem
mem_nhds_within_of_mem_nhds
{α : Type u_1}
[topological_space α]
{s t : set α}
{a : α}
(h : s ∈ 𝓝 a) :
theorem
mem_of_mem_nhds_within
{α : Type u_1}
[topological_space α]
{a : α}
{s t : set α}
(ha : a ∈ s)
(ht : t ∈ 𝓝[s] a) :
a ∈ t
theorem
filter.eventually.self_of_nhds_within
{α : Type u_1}
[topological_space α]
{p : α → Prop}
{s : set α}
{x : α}
(h : ∀ᶠ (y : α) in 𝓝[s] x, p y)
(hx : x ∈ s) :
p x
theorem
tendsto_const_nhds_within
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{l : filter β}
{s : set α}
{a : α}
(ha : a ∈ s) :
filter.tendsto (λ (x : β), a) l (𝓝[s] a)
theorem
nhds_within_eq_of_open
{α : Type u_1}
[topological_space α]
{a : α}
{s : set α}
(h₀ : a ∈ s)
(h₁ : is_open s) :
@[simp]
theorem
nhds_within_prod_eq
{α : Type u_1}
[topological_space α]
{β : Type u_2}
[topological_space β]
(a : α)
(b : β)
(s : set α)
(t : set β) :
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) :
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) :
theorem
nhds_within_pi_univ_eq
{ι : Type u_1}
{α : ι → Type u_2}
[fintype ι]
[Π (i : ι), topological_space (α i)]
(s : Π (i : ι), set (α i))
(x : Π (i : ι), α i) :
theorem
filter.tendsto.piecewise_nhds_within
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{f g : α → β}
{t : set α}
[Π (x : α), decidable (x ∈ t)]
{a : α}
{s : set α}
{l : filter β}
(h₀ : filter.tendsto f (𝓝[s ∩ t] a) l)
(h₁ : filter.tendsto g (𝓝[s ∩ tᶜ] a) l) :
filter.tendsto (t.piecewise f g) (𝓝[s] a) l
theorem
filter.tendsto.if_nhds_within
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{f g : α → β}
{p : α → Prop}
[decidable_pred p]
{a : α}
{s : set α}
{l : filter β}
(h₀ : filter.tendsto f (𝓝[s ∩ {x : α | p x}] a) l)
(h₁ : filter.tendsto g (𝓝[s ∩ {x : α | ¬p x}] a) l) :
filter.tendsto (λ (x : α), ite (p x) (f x) (g x)) (𝓝[s] a) l
theorem
tendsto_nhds_within_mono_left
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{f : α → β}
{a : α}
{s t : set α}
{l : filter β}
(hst : s ⊆ t)
(h : filter.tendsto f (𝓝[t] a) l) :
filter.tendsto f (𝓝[s] a) l
theorem
tendsto_nhds_within_mono_right
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{f : β → α}
{l : filter β}
{a : α}
{s t : set α}
(hst : s ⊆ t)
(h : filter.tendsto f l (𝓝[s] a)) :
filter.tendsto f l (𝓝[t] a)
theorem
tendsto_nhds_within_of_tendsto_nhds
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{f : α → β}
{a : α}
{s : set α}
{l : filter β}
(h : filter.tendsto f (𝓝 a) l) :
filter.tendsto f (𝓝[s] a) l
theorem
mem_closure_iff_nhds_within_ne_bot
{α : Type u_1}
[topological_space α]
{s : set α}
{x : α} :
theorem
nhds_within_ne_bot_of_mem
{α : Type u_1}
[topological_space α]
{s : set α}
{x : α}
(hx : x ∈ s) :
theorem
is_closed.mem_of_nhds_within_ne_bot
{α : Type u_1}
[topological_space α]
{s : set α}
(hs : is_closed s)
{x : α}
(hx : (𝓝[s] x).ne_bot) :
x ∈ s
theorem
dense_range.nhds_within_ne_bot
{α : Type u_1}
[topological_space α]
{ι : Type u_2}
{f : ι → α}
(h : dense_range f)
(x : α) :
theorem
closure_pi_set
{ι : Type u_1}
{α : ι → Type u_2}
[Π (i : ι), topological_space (α i)]
(I : set ι)
(s : Π (i : ι), set (α i)) :
theorem
eventually_eq_nhds_within_of_eq_on
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{f g : α → β}
{s : set α}
{a : α}
(h : set.eq_on f g s) :
theorem
set.eq_on.eventually_eq_nhds_within
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{f g : α → β}
{s : set α}
{a : α}
(h : set.eq_on f g s) :
theorem
tendsto_nhds_within_congr
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{f g : α → β}
{s : set α}
{a : α}
{l : filter β}
(hfg : ∀ (x : α), x ∈ s → f x = g x)
(hf : filter.tendsto f (𝓝[s] a) l) :
filter.tendsto g (𝓝[s] a) l
theorem
eventually_nhds_with_of_forall
{α : Type u_1}
[topological_space α]
{s : set α}
{a : α}
{p : α → Prop}
(h : ∀ (x : α), x ∈ 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 (𝓝 a))
(h2 : ∀ᶠ (x : β) in l, f x ∈ s) :
filter.tendsto f l (𝓝[s] a)
@[simp]
theorem
tendsto_nhds_within_range
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{a : α}
{l : filter β}
{f : β → α} :
filter.tendsto f l (𝓝[set.range f] a) ↔ filter.tendsto f l (𝓝 a)
theorem
filter.eventually_eq.eq_of_nhds_within
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{s : set α}
{f g : α → β}
{a : α}
(h : f =ᶠ[𝓝[s] a] g)
(hmem : a ∈ s) :
f a = g a
theorem
eventually_nhds_within_of_eventually_nhds
{α : Type u_1}
[topological_space α]
{s : set α}
{a : α}
{p : α → Prop}
(h : ∀ᶠ (x : α) in 𝓝 a, p x) :
nhds_within and subtypes #
theorem
nhds_within_eq_map_subtype_coe
{α : Type u_1}
[topological_space α]
{s : set α}
{a : α}
(h : a ∈ s) :
theorem
tendsto_nhds_within_iff_subtype
{α : Type u_1}
{β : Type u_2}
[topological_space α]
{s : set α}
{a : α}
(h : a ∈ s)
(f : α → β)
(l : filter β) :
filter.tendsto f (𝓝[s] a) l ↔ filter.tendsto (set.restrict f s) (𝓝 ⟨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 (𝓝[s] x) (𝓝 (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 (𝓝[s] x) (𝓝 (f x))
If a function is continuous within s at x, then it tends to f x within s by definition.
We register this fact for use with the dot notation, especially to use tendsto.comp as
continuous_within_at.comp will have a different meaning.
def
continuous_on
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : α → β)
(s : set α) :
Prop
A function between topological spaces is continuous on a subset s
when it's continuous at every point of s within s.
Equations
- 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 (set.restrict f s) ⟨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 (𝓝[s] x) (𝓝[t] f x)
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) :
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.prod 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_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 β}
(hf : continuous_on f s)
(hg : 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 : α → β}
(ctsf : continuous_within_at f s x) :
theorem
continuous_within_at_iff_ptendsto_res
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
(f : α → β)
{x : α}
{s : set α} :
continuous_within_at f s x ↔ filter.ptendsto (pfun.res f s) (𝓝 x) (𝓝 (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 ∈ 𝓝[s] 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 ∈ 𝓝[s] x) :
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 ∈ 𝓝 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 : s ⊆ f ⁻¹' A) :
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 (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 (insert x s) x
Alias of continuous_within_at_insert_self.
theorem
continuous_within_at.diff_iff
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s t : set α}
{x : α}
(ht : continuous_within_at f t x) :
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
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 : β → α}
(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.continuous_at
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α}
{x : α}
(h : continuous_within_at f s x)
(hs : s ∈ 𝓝 x) :
continuous_at f x
theorem
continuous_on.continuous_at
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{s : set α}
{x : α}
(h : continuous_on f s)
(hx : s ∈ 𝓝 x) :
continuous_at f x
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 : 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 : α}
(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_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 : 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 α}
(hf : continuous_on f s)
(h : 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 β}
(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 ∈ 𝓝 (f x)) :
theorem
set.left_inv_on.map_nhds_within_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{g : β → α}
{x : β}
{s : set β}
(h : set.left_inv_on f g s)
(hx : f (g x) = x)
(hf : continuous_within_at f (g '' s) (g x))
(hg : continuous_within_at g s x) :
theorem
function.left_inverse.map_nhds_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{g : β → α}
{x : β}
(h : function.left_inverse f g)
(hf : continuous_within_at f (set.range g) (g x))
(hg : continuous_at g x) :
theorem
continuous_within_at.preimage_mem_nhds_within'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f : α → β}
{x : α}
{s : set α}
{t : set β}
(h : continuous_within_at f s x)
(ht : t ∈ 𝓝[f '' s] f x) :
theorem
continuous_within_at.congr_of_eventually_eq
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{f f₁ : α → β}
{s : set α}
{x : α}
(h : continuous_within_at f s x)
(h₁ : f₁ =ᶠ[𝓝[s] x] f)
(hx : f₁ x = f x) :
continuous_within_at f₁ s x
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.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_on_open_of_generate_from
{α : Type u_1}
[topological_space α]
{β : Type u_2}
{s : set α}
{T : set (set β)}
{f : α → β}
(hs : is_open s)
(h : ∀ (t : set β), t ∈ T → is_open (s ∩ f ⁻¹' t)) :
continuous_on f s
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_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.piecewise'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{s t : set α}
{f g : α → β}
[Π (a : α), decidable (a ∈ t)]
(hpf : ∀ (a : α), a ∈ s ∩ frontier t → filter.tendsto f (𝓝[s ∩ t] a) (𝓝 (t.piecewise f g a)))
(hpg : ∀ (a : α), a ∈ s ∩ frontier t → filter.tendsto g (𝓝[s ∩ tᶜ] a) (𝓝 (t.piecewise f g a)))
(hf : continuous_on f (s ∩ t))
(hg : continuous_on g (s ∩ tᶜ)) :
continuous_on (t.piecewise f g) s
theorem
continuous_on.if'
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{s : set α}
{p : α → Prop}
{f g : α → β}
[Π (a : α), decidable (p a)]
(hpf : ∀ (a : α), a ∈ s ∩ frontier {a : α | p a} → filter.tendsto f (𝓝[s ∩ {a : α | p a}] a) (𝓝 (ite (p a) (f a) (g a))))
(hpg : ∀ (a : α), a ∈ s ∩ frontier {a : α | p a} → filter.tendsto g (𝓝[s ∩ {a : α | ¬p a}] a) (𝓝 (ite (p a) (f a) (g a))))
(hf : continuous_on f (s ∩ {a : α | p a}))
(hg : continuous_on g (s ∩ {a : α | ¬p a})) :
continuous_on (λ (a : α), ite (p a) (f a) (g a)) s
theorem
continuous_on.if
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{p : α → Prop}
[Π (a : α), decidable (p a)]
{s : set α}
{f g : α → β}
(hp : ∀ (a : α), a ∈ s ∩ frontier {a : α | p a} → f a = g a)
(hf : continuous_on f (s ∩ closure {a : α | p a}))
(hg : continuous_on g (s ∩ closure {a : α | ¬p a})) :
continuous_on (λ (a : α), ite (p a) (f a) (g a)) s
theorem
continuous_on.piecewise
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{s t : set α}
{f g : α → β}
[Π (a : α), decidable (a ∈ t)]
(ht : ∀ (a : α), a ∈ s ∩ frontier 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 (𝓝[{x : α | p x}] a) (𝓝 (ite (p a) (f a) (g a))))
(hpg : ∀ (a : α), a ∈ frontier {x : α | p x} → filter.tendsto g (𝓝[{x : α | ¬p x}] a) (𝓝 (ite (p a) (f a) (g a))))
(hf : continuous_on f {x : α | p x})
(hg : continuous_on g {x : α | ¬p x}) :
continuous (λ (a : α), ite (p a) (f a) (g a))
theorem
continuous_if
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{p : α → Prop}
{f g : α → β}
[Π (a : α), decidable (p a)]
(hp : ∀ (a : α), a ∈ frontier {x : α | p x} → f a = g a)
(hf : continuous_on f (closure {x : α | p x}))
(hg : continuous_on g (closure {x : α | ¬p x})) :
continuous (λ (a : α), ite (p a) (f a) (g a))
theorem
continuous.if
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[topological_space β]
{p : α → Prop}
{f g : α → β}
[Π (a : α), decidable (p a)]
(hp : ∀ (a : α), a ∈ frontier {x : α | p x} → f a = g a)
(hf : continuous f)
(hg : continuous g) :
continuous (λ (a : α), ite (p a) (f a) (g a))
theorem
continuous_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_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 : α × β} :