# mathlibdocumentation

topology.continuous_on

# Neighborhoods and continuity relative to a subset #

This file defines relative versions

• `nhds_within` of `nhds`
• `continuous_on` of `continuous`
• `continuous_within_at` of `continuous_at`

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 point `x`;
• `𝓟 s`: the principal filter of a set `s`;
• `𝓝[s] x`: the filter `nhds_within x s` of neighborhoods of a point `x` within a set `s`.
@[simp]
theorem nhds_bind_nhds_within {α : Type u_1} {a : α} {s : set α} :
(nhds a).bind (λ (x : α), s) = s
@[simp]
theorem eventually_nhds_nhds_within {α : Type u_1} {a : α} {s : set α} {p : α → Prop} :
(∀ᶠ (y : α) in nhds a, ∀ᶠ (x : α) in s, p x) ∀ᶠ (x : α) in s, p x
theorem eventually_nhds_within_iff {α : Type u_1} {a : α} {s : set α} {p : α → Prop} :
(∀ᶠ (x : α) in s, p x) ∀ᶠ (x : α) in nhds a, x sp x
@[simp]
theorem eventually_nhds_within_nhds_within {α : Type u_1} {a : α} {s : set α} {p : α → Prop} :
(∀ᶠ (y : α) in s, ∀ᶠ (x : α) in s, p x) ∀ᶠ (x : α) in s, p x
theorem nhds_within_eq {α : Type u_1} (a : α) (s : set α) :
s = ⨅ (t : set α) (H : t {t : set α | a t is_open t}), filter.principal (t s)
theorem nhds_within_univ {α : Type u_1} (a : α) :
theorem nhds_within_has_basis {α : Type u_1} {β : Type u_2} {p : β → Prop} {s : β → set α} {a : α} (h : (nhds a).has_basis p s) (t : set α) :
t).has_basis p (λ (i : β), s i t)
theorem nhds_within_basis_open {α : Type u_1} (a : α) (t : set α) :
t).has_basis (λ (u : set α), a u is_open u) (λ (u : set α), u t)
theorem mem_nhds_within {α : Type u_1} {t : set α} {a : α} {s : set α} :
t s ∃ (u : set α), a u u s t
theorem mem_nhds_within_iff_exists_mem_nhds_inter {α : Type u_1} {t : set α} {a : α} {s : set α} :
t s ∃ (u : set α) (H : u nhds a), u s t
theorem diff_mem_nhds_within_compl {α : Type u_1} {x : α} {s : set α} (hs : s nhds x) (t : set α) :
s \ t t
theorem diff_mem_nhds_within_diff {α : Type u_1} {x : α} {s t : set α} (hs : s t) (t' : set α) :
s \ t' (t \ t')
theorem nhds_of_nhds_within_of_nhds {α : Type u_1} {s t : set α} {a : α} (h1 : s nhds a) (h2 : t s) :
t nhds a
theorem preimage_nhds_within_coinduced' {α : Type u_1} {β : Type u_2} {π : α → β} {s : set β} {t : set α} {a : α} (h : a t) (ht : is_open t) (hs : s nhds (π a)) :
π ⁻¹' s t
theorem mem_nhds_within_of_mem_nhds {α : Type u_1} {s t : set α} {a : α} (h : s nhds a) :
s t
theorem self_mem_nhds_within {α : Type u_1} {a : α} {s : set α} :
s s
theorem inter_mem_nhds_within {α : Type u_1} (s : set α) {t : set α} {a : α} (h : t nhds a) :
s t s
theorem nhds_within_mono {α : Type u_1} (a : α) {s t : set α} (h : s t) :
s t
theorem pure_le_nhds_within {α : Type u_1} {a : α} {s : set α} (ha : a s) :
theorem mem_of_mem_nhds_within {α : Type u_1} {a : α} {s t : set α} (ha : a s) (ht : t s) :
a t
theorem filter.eventually.self_of_nhds_within {α : Type u_1} {p : α → Prop} {s : set α} {x : α} (h : ∀ᶠ (y : α) in s, p y) (hx : x s) :
p x
theorem tendsto_const_nhds_within {α : Type u_1} {β : Type u_2} {l : filter β} {s : set α} {a : α} (ha : a s) :
filter.tendsto (λ (x : β), a) l s)
theorem nhds_within_restrict'' {α : Type u_1} {a : α} (s : set α) {t : set α} (h : t s) :
s = (s t)
theorem nhds_within_restrict' {α : Type u_1} {a : α} (s : set α) {t : set α} (h : t nhds a) :
s = (s t)
theorem nhds_within_restrict {α : Type u_1} {a : α} (s : set α) {t : set α} (h₀ : a t) (h₁ : is_open t) :
s = (s t)
theorem nhds_within_le_of_mem {α : Type u_1} {a : α} {s t : set α} (h : s t) :
t s
theorem nhds_within_le_nhds {α : Type u_1} {a : α} {s : set α} :
s nhds a
theorem nhds_within_eq_nhds_within' {α : Type u_1} {a : α} {s t u : set α} (hs : s nhds a) (h₂ : t s = u s) :
t = u
theorem nhds_within_eq_nhds_within {α : Type u_1} {a : α} {s t u : set α} (h₀ : a s) (h₁ : is_open s) (h₂ : t s = u s) :
t = u
theorem is_open.nhds_within_eq {α : Type u_1} {a : α} {s : set α} (h : is_open s) (ha : a s) :
s = nhds a
theorem preimage_nhds_within_coinduced {α : Type u_1} {β : Type u_2} {π : α → β} {s : set β} {t : set α} {a : α} (h : a t) (ht : is_open t) (hs : s nhds (π a)) :
π ⁻¹' s nhds a
@[simp]
theorem nhds_within_empty {α : Type u_1} (a : α) :
theorem nhds_within_union {α : Type u_1} (a : α) (s t : set α) :
(s t) = s t
theorem nhds_within_inter {α : Type u_1} (a : α) (s t : set α) :
(s t) = s t
theorem nhds_within_inter' {α : Type u_1} (a : α) (s t : set α) :
(s t) =
theorem nhds_within_inter_of_mem {α : Type u_1} {a : α} {s t : set α} (h : s t) :
(s t) = t
@[simp]
theorem nhds_within_singleton {α : Type u_1} (a : α) :
{a} =
@[simp]
theorem nhds_within_insert {α : Type u_1} (a : α) (s : set α) :
s) =
theorem mem_nhds_within_insert {α : Type u_1} {a : α} {s t : set α} :
t s) a t t s
theorem insert_mem_nhds_within_insert {α : Type u_1} {a : α} {s t : set α} (h : t s) :
s)
theorem insert_mem_nhds_iff {α : Type u_1} {a : α} {s : set α} :
nhds a s {a}
@[simp]
theorem nhds_within_compl_singleton_sup_pure {α : Type u_1} (a : α) :
{a} = nhds a
theorem nhds_within_prod_eq {α : Type u_1} {β : Type u_2} (a : α) (b : β) (s : set α) (t : set β) :
nhds_within (a, b) (s ×ˢ t) = s).prod t)
theorem nhds_within_prod {α : Type u_1} {β : Type u_2} {s u : set α} {t v : set β} {a : α} {b : β} (hu : u s) (hv : v 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) :
(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) :
(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} [fintype ι] [Π (i : ι), topological_space (α i)] (s : Π (i : ι), set (α i)) (x : Π (i : ι), α i) :
(set.univ.pi s) = ⨅ (i : ι), filter.comap (λ (x : Π (i : ι), α i), x i) (nhds_within (x i) (s i))
theorem nhds_within_pi_eq_bot {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), topological_space (α i)] {I : set ι} {s : Π (i : ι), set (α i)} {x : Π (i : ι), α i} :
(I.pi s) = ∃ (i : ι) (H : i 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} :
(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} {f g : α → β} {t : set α} [Π (x : α), decidable (x t)] {a : α} {s : set α} {l : filter β} (h₀ : (s t)) l) (h₁ : (s t)) l) :
theorem filter.tendsto.if_nhds_within {α : Type u_1} {β : Type u_2} {f g : α → β} {p : α → Prop} {a : α} {s : set α} {l : filter β} (h₀ : (s {x : α | p x})) l) (h₁ : (s {x : α | ¬p x})) l) :
filter.tendsto (λ (x : α), ite (p x) (f x) (g x)) s) l
theorem map_nhds_within {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) (s : set α) :
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} {f : α → β} {a : α} {s t : set α} {l : filter β} (hst : s t) (h : t) l) :
s) l
theorem tendsto_nhds_within_mono_right {α : Type u_1} {β : Type u_2} {f : β → α} {l : filter β} {a : α} {s t : set α} (hst : s t) (h : s)) :
t)
theorem tendsto_nhds_within_of_tendsto_nhds {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {s : set α} {l : filter β} (h : (nhds a) l) :
s) l
theorem principal_subtype {α : Type u_1} (s : set α) (t : set {x // x s}) :
theorem nhds_within_ne_bot_of_mem {α : Type u_1} {s : set α} {x : α} (hx : x s) :
s).ne_bot
theorem is_closed.mem_of_nhds_within_ne_bot {α : Type u_1} {s : set α} (hs : is_closed s) {x : α} (hx : s).ne_bot) :
x s
theorem dense_range.nhds_within_ne_bot {α : Type u_1} {ι : Type u_2} {f : ι → α} (h : dense_range f) (x : α) :
theorem mem_closure_pi {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), topological_space (α i)] {I : set ι} {s : Π (i : ι), set (α i)} {x : Π (i : ι), α i} :
x closure (I.pi s) ∀ (i : ι), i Ix i closure (s i)
theorem closure_pi_set {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), topological_space (α i)] (I : set ι) (s : Π (i : ι), set (α i)) :
closure (I.pi s) = I.pi (λ (i : ι), closure (s i))
theorem dense_pi {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), topological_space (α i)] {s : Π (i : ι), set (α i)} (I : set ι) (hs : ∀ (i : ι), i Idense (s i)) :
dense (I.pi s)
theorem eventually_eq_nhds_within_iff {α : Type u_1} {β : Type u_2} {f g : α → β} {s : set α} {a : α} :
f =ᶠ[ s] g ∀ᶠ (x : α) in nhds a, x sf x = g x
theorem eventually_eq_nhds_within_of_eq_on {α : Type u_1} {β : Type u_2} {f g : α → β} {s : set α} {a : α} (h : g s) :
f =ᶠ[ s] g
theorem set.eq_on.eventually_eq_nhds_within {α : Type u_1} {β : Type u_2} {f g : α → β} {s : set α} {a : α} (h : g s) :
f =ᶠ[ s] g
theorem tendsto_nhds_within_congr {α : Type u_1} {β : Type u_2} {f g : α → β} {s : set α} {a : α} {l : filter β} (hfg : ∀ (x : α), x sf x = g x) (hf : s) l) :
s) l
theorem eventually_nhds_within_of_forall {α : Type u_1} {s : set α} {a : α} {p : α → Prop} (h : ∀ (x : α), x sp x) :
∀ᶠ (x : α) in s, p x
theorem tendsto_nhds_within_of_tendsto_nhds_of_eventually_within {α : Type u_1} {β : Type u_2} {a : α} {l : filter β} {s : set α} (f : β → α) (h1 : (nhds a)) (h2 : ∀ᶠ (x : β) in l, f x s) :
s)
@[simp]
theorem tendsto_nhds_within_range {α : Type u_1} {β : Type u_2} {a : α} {l : filter β} {f : β → α} :
(set.range f)) (nhds a)
theorem filter.eventually_eq.eq_of_nhds_within {α : Type u_1} {β : Type u_2} {s : set α} {f g : α → β} {a : α} (h : f =ᶠ[ s] g) (hmem : a s) :
f a = g a
theorem eventually_nhds_within_of_eventually_nhds {α : Type u_1} {s : set α} {a : α} {p : α → Prop} (h : ∀ᶠ (x : α) in nhds a, p x) :
∀ᶠ (x : α) in s, p x

### `nhds_within` and subtypes #

theorem mem_nhds_within_subtype {α : Type u_1} {s : set α} {a : {x // x s}} {t u : set {x // x s}} :
t u t (coe '' u))
theorem nhds_within_subtype {α : Type u_1} (s : set α) (a : {x // x s}) (t : set {x // x s}) :
t = (coe '' t))
theorem nhds_within_eq_map_subtype_coe {α : Type u_1} {s : set α} {a : α} (h : a s) :
s = (nhds a, h⟩)
theorem mem_nhds_subtype_iff_nhds_within {α : Type u_1} {s : set α} {a : s} {t : set s} :
t nhds a s
theorem preimage_coe_mem_nhds_subtype {α : Type u_1} {s t : set α} {a : s} :
nhds a t s
theorem tendsto_nhds_within_iff_subtype {α : Type u_1} {β : Type u_2} {s : set α} {a : α} (h : a s) (f : α → β) (l : filter β) :
s) l filter.tendsto (s.restrict f) (nhds a, h⟩) l
def continuous_within_at {α : Type u_1} {β : Type u_2} (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
theorem continuous_within_at.tendsto {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {x : α} (h : 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} (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
• = ∀ (x : α), x s x
theorem continuous_on.continuous_within_at {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {x : α} (hf : s) (hx : x s) :
x
theorem continuous_within_at_univ {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) :
theorem continuous_within_at_iff_continuous_at_restrict {α : Type u_1} {β : Type u_2} (f : α → β) {x : α} {s : set α} (h : x s) :
x continuous_at (s.restrict f) x, h⟩
theorem continuous_within_at.tendsto_nhds_within {α : Type u_1} {β : Type u_2} {f : α → β} {x : α} {s : set α} {t : set β} (h : x) (ht : s t) :
s) (nhds_within (f x) t)
theorem continuous_within_at.tendsto_nhds_within_image {α : Type u_1} {β : Type u_2} {f : α → β} {x : α} {s : set α} (h : 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} {f : α → γ} {g : β → δ} {s : set α} {t : set β} {x : α} {y : β} (hf : x) (hg : y) :
(s ×ˢ t) (x, y)
theorem continuous_within_at_pi {α : Type u_1} {ι : Type u_2} {π : ι → Type u_3} [Π (i : ι), topological_space (π i)] {f : α → Π (i : ι), π i} {s : set α} {x : α} :
x ∀ (i : ι), continuous_within_at (λ (y : α), f y i) s x
theorem continuous_on_pi {α : Type u_1} {ι : Type u_2} {π : ι → Type u_3} [Π (i : ι), topological_space (π i)] {f : α → Π (i : ι), π i} {s : set α} :
∀ (i : ι), continuous_on (λ (y : α), f y i) s
theorem continuous_within_at.fin_insert_nth {α : Type u_1} {n : } {π : fin (n + 1)Type u_2} [Π (i : fin (n + 1)), topological_space (π i)] (i : fin (n + 1)) {f : α → π i} {a : α} {s : set α} (hf : a) {g : α → Π (j : fin n), π ((i.succ_above) j)} (hg : a) :
continuous_within_at (λ (a : α), i.insert_nth (f a) (g a)) s a
theorem continuous_on.fin_insert_nth {α : Type u_1} {n : } {π : fin (n + 1)Type u_2} [Π (i : fin (n + 1)), topological_space (π i)] (i : fin (n + 1)) {f : α → π i} {s : set α} (hf : s) {g : α → Π (j : fin n), π ((i.succ_above) j)} (hg : s) :
continuous_on (λ (a : α), i.insert_nth (f a) (g a)) s
theorem continuous_on_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} :
∀ (x : α), x s∀ (t : set β), f x t(∃ (u : set α), x u u s f ⁻¹' t)
theorem continuous_on_iff_continuous_restrict {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} :
theorem continuous_on_iff' {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} :
∀ (t : set β), (∃ (u : set α), f ⁻¹' t s = u s)
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₂ : 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₂ : 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_iff_is_closed {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} :
∀ (t : set β), (∃ (u : set α), f ⁻¹' t s = u s)
theorem continuous_on.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} {s : set α} {t : set β} (hf : s) (hg : t) :
theorem continuous_on_empty {α : Type u_1} {β : Type u_2} (f : α → β) :
theorem continuous_on_singleton {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) :
{a}
theorem set.subsingleton.continuous_on {α : Type u_1} {β : Type u_2} {s : set α} (hs : s.subsingleton) (f : α → β) :
theorem nhds_within_le_comap {α : Type u_1} {β : Type u_2} {x : α} {s : set α} {f : α → β} (ctsf : x) :
s (nhds_within (f x) (f '' s))
@[simp]
theorem comap_nhds_within_range {β : Type u_2} {α : Type u_1} (f : α → β) (y : β) :
(set.range f)) = (nhds y)
theorem continuous_within_at_iff_ptendsto_res {α : Type u_1} {β : Type u_2} (f : α → β) {x : α} {s : set α} :
x filter.ptendsto (pfun.res f s) (nhds x) (nhds (f x))
theorem continuous_iff_continuous_on_univ {α : Type u_1} {β : Type u_2} {f : α → β} :
theorem continuous_within_at.mono {α : Type u_1} {β : Type u_2} {f : α → β} {s t : set α} {x : α} (h : x) (hs : s t) :
x
theorem continuous_within_at.mono_of_mem {α : Type u_1} {β : Type u_2} {f : α → β} {s t : set α} {x : α} (h : x) (hs : t s) :
x
theorem continuous_within_at_inter' {α : Type u_1} {β : Type u_2} {f : α → β} {s t : set α} {x : α} (h : t s) :
(s t) x x
theorem continuous_within_at_inter {α : Type u_1} {β : Type u_2} {f : α → β} {s t : set α} {x : α} (h : t nhds x) :
(s t) x x
theorem continuous_within_at_union {α : Type u_1} {β : Type u_2} {f : α → β} {s t : set α} {x : α} :
(s t) x x x
theorem continuous_within_at.union {α : Type u_1} {β : Type u_2} {f : α → β} {s t : set α} {x : α} (hs : x) (ht : x) :
(s t) x
theorem continuous_within_at.mem_closure_image {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {x : α} (h : x) (hx : x ) :
f x closure (f '' s)
theorem continuous_within_at.mem_closure {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {x : α} {A : set β} (h : x) (hx : x ) (hA : s A) :
f x
theorem set.maps_to.closure_of_continuous_within_at {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {t : set β} (h : s t) (hc : ∀ (x : α), x x) :
(closure s) (closure t)
theorem set.maps_to.closure_of_continuous_on {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {t : set β} (h : s t) (hc : (closure s)) :
(closure s) (closure t)
theorem continuous_within_at.image_closure {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} (hf : ∀ (x : α), x x) :
f '' closure (f '' s)
theorem continuous_on.image_closure {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} (hf : (closure s)) :
f '' closure (f '' s)
@[simp]
theorem continuous_within_at_singleton {α : Type u_1} {β : Type u_2} {f : α → β} {x : α} :
{x} x
@[simp]
theorem continuous_within_at_insert_self {α : Type u_1} {β : Type u_2} {f : α → β} {x : α} {s : set α} :
x x
theorem continuous_within_at.insert_self {α : Type u_1} {β : Type u_2} {f : α → β} {x : α} {s : set α} :
x x

Alias of the reverse direction of `continuous_within_at_insert_self`.

theorem continuous_within_at.diff_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s t : set α} {x : α} (ht : x) :
(s \ t) x x
@[simp]
theorem continuous_within_at_diff_self {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {x : α} :
(s \ {x}) x x
@[simp]
theorem continuous_within_at_compl_self {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} :
a
@[simp]
theorem continuous_within_at_update_same {α : Type u_1} {β : Type u_2} [decidable_eq α] {f : α → β} {s : set α} {x : α} {y : β} :
s x (s \ {x})) (nhds y)
@[simp]
theorem continuous_at_update_same {α : Type u_1} {β : Type u_2} [decidable_eq α] {f : α → β} {x : α} {y : β} :
continuous_at x y) x {x}) (nhds y)
theorem is_open_map.continuous_on_image_of_left_inv_on {α : Type u_1} {β : Type u_2} {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} {f : α → β} (hf : is_open_map f) {finv : β → α} (hleft : f) :
theorem continuous_on.congr_mono {α : Type u_1} {β : Type u_2} {f g : α → β} {s s₁ : set α} (h : s) (h' : f s₁) (h₁ : s₁ s) :
s₁
theorem continuous_on.congr {α : Type u_1} {β : Type u_2} {f g : α → β} {s : set α} (h : s) (h' : f s) :
theorem continuous_on_congr {α : Type u_1} {β : Type u_2} {f g : α → β} {s : set α} (h' : f s) :
theorem continuous_at.continuous_within_at {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {x : α} (h : x) :
x
theorem continuous_within_at_iff_continuous_at {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {x : α} (h : s nhds x) :
x
theorem continuous_within_at.continuous_at {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {x : α} (h : x) (hs : s nhds x) :
theorem continuous_on.continuous_at {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {x : α} (h : s) (hx : s nhds x) :
theorem continuous_at.continuous_on {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} (hcont : ∀ (x : α), x s) :
theorem continuous_within_at.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {f : α → β} {s : set α} {t : set β} {x : α} (hg : (f x)) (hf : x) (h : s t) :
theorem continuous_within_at.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {f : α → β} {s : set α} {t : set β} {x : α} (hg : (f x)) (hf : x) :
theorem continuous_at.comp_continuous_within_at {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {f : α → β} {s : set α} {x : α} (hg : (f x)) (hf : x) :
theorem continuous_on.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {f : α → β} {s : set α} {t : set β} (hg : t) (hf : s) (h : s t) :
theorem continuous_on.mono {α : Type u_1} {β : Type u_2} {f : α → β} {s t : set α} (hf : s) (h : t s) :
theorem antitone_continuous_on {α : Type u_1} {β : Type u_2} {f : α → β} :
theorem continuous_on.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {f : α → β} {s : set α} {t : set β} (hg : t) (hf : s) :
continuous_on (g f) (s f ⁻¹' t)
theorem continuous.continuous_on {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} (h : continuous f) :
theorem continuous.continuous_within_at {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {x : α} (h : continuous f) :
x
theorem continuous.comp_continuous_on {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {f : α → β} {s : set α} (hg : continuous g) (hf : s) :
theorem continuous_on.comp_continuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {f : α → β} {s : set β} (hg : s) (hf : continuous f) (hs : ∀ (x : α), f x s) :
theorem continuous_within_at.preimage_mem_nhds_within {α : Type u_1} {β : Type u_2} {f : α → β} {x : α} {s : set α} {t : set β} (h : x) (ht : t nhds (f x)) :
f ⁻¹' t s
theorem set.left_inv_on.map_nhds_within_eq {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} {x : β} {s : set β} (h : s) (hx : f (g x) = x) (hf : (g '' s) (g x)) (hg : x) :
s) = nhds_within (g x) (g '' s)
theorem function.left_inverse.map_nhds_eq {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} {x : β} (h : g) (hf : (g x)) (hg : x) :
(nhds x) = nhds_within (g x) (set.range g)
theorem continuous_within_at.preimage_mem_nhds_within' {α : Type u_1} {β : Type u_2} {f : α → β} {x : α} {s : set α} {t : set β} (h : x) (ht : t nhds_within (f x) (f '' s)) :
f ⁻¹' t s
theorem filter.eventually_eq.congr_continuous_within_at {α : Type u_1} {β : Type u_2} {f g : α → β} {s : set α} {x : α} (h : f =ᶠ[ s] g) (hx : f x = g x) :
x x
theorem continuous_within_at.congr_of_eventually_eq {α : Type u_1} {β : Type u_2} {f f₁ : α → β} {s : set α} {x : α} (h : x) (h₁ : f₁ =ᶠ[ s] f) (hx : f₁ x = f x) :
x
theorem continuous_within_at.congr {α : Type u_1} {β : Type u_2} {f f₁ : α → β} {s : set α} {x : α} (h : x) (h₁ : ∀ (y : α), y sf₁ y = f y) (hx : f₁ x = f x) :
x
theorem continuous_within_at.congr_mono {α : Type u_1} {β : Type u_2} {f g : α → β} {s s₁ : set α} {x : α} (h : x) (h' : f s₁) (h₁ : s₁ s) (hx : g x = f x) :
x
theorem continuous_on_const {α : Type u_1} {β : Type u_2} {s : set α} {c : β} :
continuous_on (λ (x : α), c) s
theorem continuous_within_at_const {α : Type u_1} {β : Type u_2} {b : β} {s : set α} {x : α} :
continuous_within_at (λ (_x : α), b) s x
theorem continuous_on_id {α : Type u_1} {s : set α} :
theorem continuous_within_at_id {α : Type u_1} {s : set α} {x : α} :
theorem continuous_on_open_iff {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} (hs : is_open s) :
∀ (t : set β), is_open (s f ⁻¹' t)
theorem continuous_on.preimage_open_of_open {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {t : set β} (hf : s) (hs : is_open s) (ht : is_open t) :
theorem continuous_on.is_open_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {t : set β} (h : 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} {f : α → β} {s : set α} {t : set β} (hf : s) (hs : is_closed s) (ht : is_closed t) :
theorem continuous_on.preimage_interior_subset_interior_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {t : set β} (hf : s) (hs : is_open s) :
theorem continuous_on_of_locally_continuous_on {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} (h : ∀ (x : α), x s(∃ (t : set α), x t (s t))) :
theorem continuous_on_open_of_generate_from {α : Type u_1} {β : Type u_2} {s : set α} {T : set (set β)} {f : α → β} (hs : is_open s) (h : ∀ (t : set β), t Tis_open (s f ⁻¹' t)) :
theorem continuous_within_at.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {s : set α} {x : α} (hf : x) (hg : x) :
continuous_within_at (λ (x : α), (f x, g x)) s x
theorem continuous_on.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {s : set α} (hf : s) (hg : s) :
continuous_on (λ (x : α), (f x, g x)) s
theorem inducing.continuous_within_at_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} (hg : inducing g) {s : set α} {x : α} :
theorem inducing.continuous_on_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} (hg : inducing g) {s : set α} :
theorem embedding.continuous_on_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} (hg : embedding g) {s : set α} :
theorem embedding.map_nhds_within_eq {α : Type u_1} {β : Type u_2} {f : α → β} (hf : embedding f) (s : set α) (x : α) :
s) = nhds_within (f x) (f '' s)
theorem open_embedding.map_nhds_within_preimage_eq {α : Type u_1} {β : Type u_2} {f : α → β} (hf : open_embedding f) (s : set β) (x : α) :
(f ⁻¹' s)) = nhds_within (f x) s
theorem continuous_within_at_of_not_mem_closure {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {x : α} :
x x
theorem continuous_on.piecewise' {α : Type u_1} {β : Type u_2} {s t : set α} {f g : α → β} [Π (a : α), decidable (a t)] (hpf : ∀ (a : α), a s (s t)) (nhds (t.piecewise f g a))) (hpg : ∀ (a : α), a s (s t)) (nhds (t.piecewise f g a))) (hf : (s t)) (hg : (s t)) :
theorem continuous_on.if' {α : Type u_1} {β : Type u_2} {s : set α} {p : α → Prop} {f g : α → β} [Π (a : α), decidable (p a)] (hpf : ∀ (a : α), a s frontier {a : α | p a} (s {a : α | p a})) (nhds (ite (p a) (f a) (g a)))) (hpg : ∀ (a : α), a s frontier {a : α | p a} (s {a : α | ¬p a})) (nhds (ite (p a) (f a) (g a)))) (hf : (s {a : α | p a})) (hg : (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} {p : α → Prop} [Π (a : α), decidable (p a)] {s : set α} {f g : α → β} (hp : ∀ (a : α), a s frontier {a : α | p a}f a = g a) (hf : (s closure {a : α | p a})) (hg : (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} {s t : set α} {f g : α → β} [Π (a : α), decidable (a t)] (ht : ∀ (a : α), a s f a = g a) (hf : (s closure t)) (hg : (s closure t)) :
theorem continuous_if' {α : Type u_1} {β : Type u_2} {p : α → Prop} {f g : α → β} [Π (a : α), decidable (p a)] (hpf : ∀ (a : α), a frontier {x : α | p x} {x : α | p x}) (nhds (ite (p a) (f a) (g a)))) (hpg : ∀ (a : α), a frontier {x : α | p x} {x : α | ¬p x}) (nhds (ite (p a) (f a) (g a)))) (hf : {x : α | p x}) (hg : {x : α | ¬p x}) :
continuous (λ (a : α), ite (p a) (f a) (g a))
theorem continuous_if {α : Type u_1} {β : Type u_2} {p : α → Prop} {f g : α → β} [Π (a : α), decidable (p a)] (hp : ∀ (a : α), a frontier {x : α | p x}f a = g a) (hf : (closure {x : α | p x})) (hg : (closure {x : α | ¬p x})) :
continuous (λ (a : α), ite (p a) (f a) (g a))
theorem continuous.if {α : Type u_1} {β : Type u_2} {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} (p : Prop) {f g : α → β} [decidable p] (hf : p → ) (hg : ¬p → ) :
continuous (λ (a : α), ite p (f a) (g a))
theorem continuous.if_const {α : Type u_1} {β : Type u_2} (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} {s : set α} {f g : α → β} [Π (a : α), decidable (a s)] (hs : ∀ (a : α), a f a = g a) (hf : (closure s)) (hg : (closure s)) :
theorem continuous.piecewise {α : Type u_1} {β : Type u_2} {s : set α} {f g : α → β} [Π (a : α), decidable (a s)] (hs : ∀ (a : α), a f a = g a) (hf : continuous f) (hg : continuous g) :
theorem is_open.ite' {α : Type u_1} {s s' t : set α} (hs : is_open s) (hs' : is_open s') (ht : ∀ (x : α), x (x s x s')) :
is_open (t.ite s s')
theorem is_open.ite {α : Type u_1} {s s' t : set α} (hs : is_open s) (hs' : is_open s') (ht : s = s' ) :
is_open (t.ite s s')
theorem ite_inter_closure_eq_of_inter_frontier_eq {α : Type u_1} {s s' t : set α} (ht : s = s' ) :
t.ite s s' = s
theorem ite_inter_closure_compl_eq_of_inter_frontier_eq {α : Type u_1} {s s' t : set α} (ht : s = s' ) :
t.ite s s' = s'
theorem continuous_on_piecewise_ite' {α : Type u_1} {β : Type u_2} {s s' t : set α} {f f' : α → β} [Π (x : α), decidable (x t)] (h : (s closure t)) (h' : (s' closure t)) (H : s = s' ) (Heq : 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} {s s' t : set α} {f f' : α → β} [Π (x : α), decidable (x t)] (h : s) (h' : s') (H : s = s' ) (Heq : f' (s frontier t)) :
continuous_on (t.piecewise f f') (t.ite s s')
theorem frontier_inter_open_inter {α : Type u_1} {s t : set α} (ht : is_open t) :
frontier (s t) t = t
theorem continuous_on_fst {α : Type u_1} {β : Type u_2} {s : set × β)} :
theorem continuous_within_at_fst {α : Type u_1} {β : Type u_2} {s : set × β)} {p : α × β} :
theorem continuous_on.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β × γ} {s : set α} (hf : s) :
continuous_on (λ (x : α), (f x).fst) s
theorem continuous_within_at.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β × γ} {s : set α} {a : α} (h : a) :
continuous_within_at (λ (x : α), (f x).fst) s a
theorem continuous_on_snd {α : Type u_1} {β : Type u_2} {s : set × β)} :
theorem continuous_within_at_snd {α : Type u_1} {β : Type u_2} {s : set × β)} {p : α × β} :
theorem continuous_on.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β × γ} {s : set α} (hf : s) :
continuous_on (λ (x : α), (f x).snd) s
theorem continuous_within_at.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β × γ} {s : set α} {a : α} (h : 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} {f : α → β × γ} {s : set α} {x : α} :
x x x