Documentation

Mathlib.Topology.ContinuousOn

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 #

@[simp]
theorem nhds_bind_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} :
((nhds a).bind fun (x : α) => nhdsWithin x s) = nhdsWithin a s
@[simp]
theorem eventually_nhds_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {p : αProp} :
(∀ᶠ (y : α) in nhds a, ∀ᶠ (x : α) in nhdsWithin y s, p x) ∀ᶠ (x : α) in nhdsWithin a s, p x
theorem eventually_nhdsWithin_iff {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {p : αProp} :
(∀ᶠ (x : α) in nhdsWithin a s, p x) ∀ᶠ (x : α) in nhds a, x sp x
theorem frequently_nhdsWithin_iff {α : Type u_1} [TopologicalSpace α] {z : α} {s : Set α} {p : αProp} :
(∃ᶠ (x : α) in nhdsWithin z s, p x) ∃ᶠ (x : α) in nhds z, p x x s
theorem mem_closure_ne_iff_frequently_within {α : Type u_1} [TopologicalSpace α] {z : α} {s : Set α} :
z closure (s \ {z}) ∃ᶠ (x : α) in nhdsWithin z {z}, x s
@[simp]
theorem eventually_nhdsWithin_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {p : αProp} :
(∀ᶠ (y : α) in nhdsWithin a s, ∀ᶠ (x : α) in nhdsWithin y s, p x) ∀ᶠ (x : α) in nhdsWithin a s, p x
theorem nhdsWithin_eq {α : Type u_1} [TopologicalSpace α] (a : α) (s : Set α) :
nhdsWithin a s = t{t : Set α | a t IsOpen t}, Filter.principal (t s)
theorem nhdsWithin_univ {α : Type u_1} [TopologicalSpace α] (a : α) :
nhdsWithin a Set.univ = nhds a
theorem nhdsWithin_hasBasis {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {p : βProp} {s : βSet α} {a : α} (h : (nhds a).HasBasis p s) (t : Set α) :
(nhdsWithin a t).HasBasis p fun (i : β) => s i t
theorem nhdsWithin_basis_open {α : Type u_1} [TopologicalSpace α] (a : α) (t : Set α) :
(nhdsWithin a t).HasBasis (fun (u : Set α) => a u IsOpen u) fun (u : Set α) => u t
theorem mem_nhdsWithin {α : Type u_1} [TopologicalSpace α] {t : Set α} {a : α} {s : Set α} :
t nhdsWithin a s ∃ (u : Set α), IsOpen u a u u s t
theorem mem_nhdsWithin_iff_exists_mem_nhds_inter {α : Type u_1} [TopologicalSpace α] {t : Set α} {a : α} {s : Set α} :
t nhdsWithin a s unhds a, u s t
theorem diff_mem_nhdsWithin_compl {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} (hs : s nhds x) (t : Set α) :
theorem diff_mem_nhdsWithin_diff {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} {t : Set α} (hs : s nhdsWithin x t) (t' : Set α) :
s \ t' nhdsWithin x (t \ t')
theorem nhds_of_nhdsWithin_of_nhds {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} {a : α} (h1 : s nhds a) (h2 : t nhdsWithin a s) :
t nhds a
theorem mem_nhdsWithin_iff_eventually {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} {x : α} :
t nhdsWithin x s ∀ᶠ (y : α) in nhds x, y sy t
theorem mem_nhdsWithin_iff_eventuallyEq {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} {x : α} :
theorem nhdsWithin_eq_iff_eventuallyEq {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} {x : α} :
theorem nhdsWithin_le_iff {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} {x : α} :
theorem preimage_nhdsWithin_coinduced' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {π : αβ} {s : Set β} {t : Set α} {a : α} (h : a t) (hs : s nhds (π a)) :
theorem mem_nhdsWithin_of_mem_nhds {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} {a : α} (h : s nhds a) :
theorem self_mem_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} :
theorem eventually_mem_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} :
∀ᶠ (x : α) in nhdsWithin a s, x s
theorem inter_mem_nhdsWithin {α : Type u_1} [TopologicalSpace α] (s : Set α) {t : Set α} {a : α} (h : t nhds a) :
theorem nhdsWithin_mono {α : Type u_1} [TopologicalSpace α] (a : α) {s : Set α} {t : Set α} (h : s t) :
theorem pure_le_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} (ha : a s) :
theorem mem_of_mem_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {t : Set α} (ha : a s) (ht : t nhdsWithin a s) :
a t
theorem Filter.Eventually.self_of_nhdsWithin {α : Type u_1} [TopologicalSpace α] {p : αProp} {s : Set α} {x : α} (h : ∀ᶠ (y : α) in nhdsWithin x s, p y) (hx : x s) :
p x
theorem tendsto_const_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {l : Filter β} {s : Set α} {a : α} (ha : a s) :
Filter.Tendsto (fun (x : β) => a) l (nhdsWithin a s)
theorem nhdsWithin_restrict'' {α : Type u_1} [TopologicalSpace α] {a : α} (s : Set α) {t : Set α} (h : t nhdsWithin a s) :
theorem nhdsWithin_restrict' {α : Type u_1} [TopologicalSpace α] {a : α} (s : Set α) {t : Set α} (h : t nhds a) :
theorem nhdsWithin_restrict {α : Type u_1} [TopologicalSpace α] {a : α} (s : Set α) {t : Set α} (h₀ : a t) (h₁ : IsOpen t) :
theorem nhdsWithin_le_of_mem {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {t : Set α} (h : s nhdsWithin a t) :
theorem nhdsWithin_le_nhds {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} :
theorem nhdsWithin_eq_nhdsWithin' {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {t : Set α} {u : Set α} (hs : s nhds a) (h₂ : t s = u s) :
theorem nhdsWithin_eq_nhdsWithin {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {t : Set α} {u : Set α} (h₀ : a s) (h₁ : IsOpen s) (h₂ : t s = u s) :
@[simp]
theorem nhdsWithin_eq_nhds {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} :
theorem IsOpen.nhdsWithin_eq {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} (h : IsOpen s) (ha : a s) :
theorem preimage_nhds_within_coinduced {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {π : αβ} {s : Set β} {t : Set α} {a : α} (h : a t) (ht : IsOpen t) (hs : s nhds (π a)) :
π ⁻¹' s nhds a
@[simp]
theorem nhdsWithin_empty {α : Type u_1} [TopologicalSpace α] (a : α) :
theorem nhdsWithin_union {α : Type u_1} [TopologicalSpace α] (a : α) (s : Set α) (t : Set α) :
theorem nhdsWithin_biUnion {α : Type u_1} [TopologicalSpace α] {ι : Type u_5} {I : Set ι} (hI : I.Finite) (s : ιSet α) (a : α) :
nhdsWithin a (iI, s i) = iI, nhdsWithin a (s i)
theorem nhdsWithin_sUnion {α : Type u_1} [TopologicalSpace α] {S : Set (Set α)} (hS : S.Finite) (a : α) :
nhdsWithin a (⋃₀ S) = sS, nhdsWithin a s
theorem nhdsWithin_iUnion {α : Type u_1} [TopologicalSpace α] {ι : Sort u_5} [Finite ι] (s : ιSet α) (a : α) :
nhdsWithin a (⋃ (i : ι), s i) = ⨆ (i : ι), nhdsWithin a (s i)
theorem nhdsWithin_inter {α : Type u_1} [TopologicalSpace α] (a : α) (s : Set α) (t : Set α) :
theorem nhdsWithin_inter' {α : Type u_1} [TopologicalSpace α] (a : α) (s : Set α) (t : Set α) :
theorem nhdsWithin_inter_of_mem {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {t : Set α} (h : s nhdsWithin a t) :
theorem nhdsWithin_inter_of_mem' {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {t : Set α} (h : t nhdsWithin a s) :
@[simp]
theorem nhdsWithin_singleton {α : Type u_1} [TopologicalSpace α] (a : α) :
nhdsWithin a {a} = pure a
@[simp]
theorem nhdsWithin_insert {α : Type u_1} [TopologicalSpace α] (a : α) (s : Set α) :
theorem mem_nhdsWithin_insert {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {t : Set α} :
theorem insert_mem_nhdsWithin_insert {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {t : Set α} (h : t nhdsWithin a s) :
theorem insert_mem_nhds_iff {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} :
@[simp]
theorem nhdsWithin_prod {α : Type u_5} [TopologicalSpace α] {β : Type u_6} [TopologicalSpace β] {s : Set α} {u : Set α} {t : Set β} {v : Set β} {a : α} {b : β} (hu : u nhdsWithin a s) (hv : v nhdsWithin b t) :
u ×ˢ v nhdsWithin (a, b) (s ×ˢ t)
theorem nhdsWithin_pi_eq' {ι : Type u_5} {α : ιType u_6} [(i : ι) → TopologicalSpace (α i)] {I : Set ι} (hI : I.Finite) (s : (i : ι) → Set (α i)) (x : (i : ι) → α i) :
nhdsWithin x (I.pi s) = ⨅ (i : ι), Filter.comap (fun (x : (i : ι) → α i) => x i) (nhds (x i) ⨅ (_ : i I), Filter.principal (s i))
theorem nhdsWithin_pi_eq {ι : Type u_5} {α : ιType u_6} [(i : ι) → TopologicalSpace (α i)] {I : Set ι} (hI : I.Finite) (s : (i : ι) → Set (α i)) (x : (i : ι) → α i) :
nhdsWithin x (I.pi s) = (iI, Filter.comap (fun (x : (i : ι) → α i) => x i) (nhdsWithin (x i) (s i))) ⨅ (i : ι), ⨅ (_ : iI), Filter.comap (fun (x : (i : ι) → α i) => x i) (nhds (x i))
theorem nhdsWithin_pi_univ_eq {ι : Type u_5} {α : ιType u_6} [Finite ι] [(i : ι) → TopologicalSpace (α i)] (s : (i : ι) → Set (α i)) (x : (i : ι) → α i) :
nhdsWithin x (Set.univ.pi s) = ⨅ (i : ι), Filter.comap (fun (x : (i : ι) → α i) => x i) (nhdsWithin (x i) (s i))
theorem nhdsWithin_pi_eq_bot {ι : Type u_5} {α : ιType u_6} [(i : ι) → TopologicalSpace (α i)] {I : Set ι} {s : (i : ι) → Set (α i)} {x : (i : ι) → α i} :
nhdsWithin x (I.pi s) = iI, nhdsWithin (x i) (s i) =
theorem nhdsWithin_pi_neBot {ι : Type u_5} {α : ιType u_6} [(i : ι) → TopologicalSpace (α i)] {I : Set ι} {s : (i : ι) → Set (α i)} {x : (i : ι) → α i} :
(nhdsWithin x (I.pi s)).NeBot iI, (nhdsWithin (x i) (s i)).NeBot
theorem Filter.Tendsto.piecewise_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : αβ} {g : αβ} {t : Set α} [(x : α) → Decidable (x t)] {a : α} {s : Set α} {l : Filter β} (h₀ : Filter.Tendsto f (nhdsWithin a (s t)) l) (h₁ : Filter.Tendsto g (nhdsWithin a (s t)) l) :
Filter.Tendsto (t.piecewise f g) (nhdsWithin a s) l
theorem Filter.Tendsto.if_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : αβ} {g : αβ} {p : αProp} [DecidablePred p] {a : α} {s : Set α} {l : Filter β} (h₀ : Filter.Tendsto f (nhdsWithin a (s {x : α | p x})) l) (h₁ : Filter.Tendsto g (nhdsWithin a (s {x : α | ¬p x})) l) :
Filter.Tendsto (fun (x : α) => if p x then f x else g x) (nhdsWithin a s) l
theorem map_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] (f : αβ) (a : α) (s : Set α) :
Filter.map f (nhdsWithin a s) = t{t : Set α | a t IsOpen t}, Filter.principal (f '' (t s))
theorem tendsto_nhdsWithin_mono_left {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : αβ} {a : α} {s : Set α} {t : Set α} {l : Filter β} (hst : s t) (h : Filter.Tendsto f (nhdsWithin a t) l) :
theorem tendsto_nhdsWithin_mono_right {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : βα} {l : Filter β} {a : α} {s : Set α} {t : Set α} (hst : s t) (h : Filter.Tendsto f l (nhdsWithin a s)) :
theorem tendsto_nhdsWithin_of_tendsto_nhds {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : αβ} {a : α} {s : Set α} {l : Filter β} (h : Filter.Tendsto f (nhds a) l) :
theorem eventually_mem_of_tendsto_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : βα} {a : α} {s : Set α} {l : Filter β} (h : Filter.Tendsto f l (nhdsWithin a s)) :
∀ᶠ (i : β) in l, f i s
theorem tendsto_nhds_of_tendsto_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : βα} {a : α} {s : Set α} {l : Filter β} (h : Filter.Tendsto f l (nhdsWithin a s)) :
theorem nhdsWithin_neBot_of_mem {α : Type u_1} [TopologicalSpace α] {s : Set α} {x : α} (hx : x s) :
(nhdsWithin x s).NeBot
theorem IsClosed.mem_of_nhdsWithin_neBot {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : IsClosed s) {x : α} (hx : (nhdsWithin x s).NeBot) :
x s
theorem DenseRange.nhdsWithin_neBot {α : Type u_1} [TopologicalSpace α] {ι : Type u_5} {f : ια} (h : DenseRange f) (x : α) :
(nhdsWithin x (Set.range f)).NeBot
theorem mem_closure_pi {ι : Type u_5} {α : ιType u_6} [(i : ι) → TopologicalSpace (α i)] {I : Set ι} {s : (i : ι) → Set (α i)} {x : (i : ι) → α i} :
x closure (I.pi s) iI, x i closure (s i)
theorem closure_pi_set {ι : Type u_5} {α : ιType u_6} [(i : ι) → TopologicalSpace (α i)] (I : Set ι) (s : (i : ι) → Set (α i)) :
closure (I.pi s) = I.pi fun (i : ι) => closure (s i)
theorem dense_pi {ι : Type u_5} {α : ιType u_6} [(i : ι) → TopologicalSpace (α i)] {s : (i : ι) → Set (α i)} (I : Set ι) (hs : iI, Dense (s i)) :
Dense (I.pi s)
theorem eventuallyEq_nhdsWithin_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : αβ} {g : αβ} {s : Set α} {a : α} :
f =ᶠ[nhdsWithin a s] g ∀ᶠ (x : α) in nhds a, x sf x = g x
theorem eventuallyEq_nhdsWithin_of_eqOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : αβ} {g : αβ} {s : Set α} {a : α} (h : Set.EqOn f g s) :
theorem Set.EqOn.eventuallyEq_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : αβ} {g : αβ} {s : Set α} {a : α} (h : Set.EqOn f g s) :
theorem tendsto_nhdsWithin_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : αβ} {g : αβ} {s : Set α} {a : α} {l : Filter β} (hfg : xs, f x = g x) (hf : Filter.Tendsto f (nhdsWithin a s) l) :
theorem eventually_nhdsWithin_of_forall {α : Type u_1} [TopologicalSpace α] {s : Set α} {a : α} {p : αProp} (h : xs, p x) :
∀ᶠ (x : α) in nhdsWithin a s, p x
theorem tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {a : α} {l : Filter β} {s : Set α} (f : βα) (h1 : Filter.Tendsto f l (nhds a)) (h2 : ∀ᶠ (x : β) in l, f x s) :
theorem tendsto_nhdsWithin_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {a : α} {l : Filter β} {s : Set α} {f : βα} :
Filter.Tendsto f l (nhdsWithin a s) Filter.Tendsto f l (nhds a) ∀ᶠ (n : β) in l, f n s
@[simp]
theorem tendsto_nhdsWithin_range {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {a : α} {l : Filter β} {f : βα} :
theorem Filter.EventuallyEq.eq_of_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {s : Set α} {f : αβ} {g : αβ} {a : α} (h : f =ᶠ[nhdsWithin a s] g) (hmem : a s) :
f a = g a
theorem eventually_nhdsWithin_of_eventually_nhds {α : Type u_5} [TopologicalSpace α] {s : Set α} {a : α} {p : αProp} (h : ∀ᶠ (x : α) in nhds a, p x) :
∀ᶠ (x : α) in nhdsWithin a s, p x

nhdsWithin and subtypes #

theorem mem_nhdsWithin_subtype {α : Type u_1} [TopologicalSpace α] {s : Set α} {a : { x : α // x s }} {t : Set { x : α // x s }} {u : Set { x : α // x s }} :
t nhdsWithin a u t Filter.comap Subtype.val (nhdsWithin (a) (Subtype.val '' u))
theorem nhdsWithin_subtype {α : Type u_1} [TopologicalSpace α] (s : Set α) (a : { x : α // x s }) (t : Set { x : α // x s }) :
nhdsWithin a t = Filter.comap Subtype.val (nhdsWithin (a) (Subtype.val '' t))
theorem nhdsWithin_eq_map_subtype_coe {α : Type u_1} [TopologicalSpace α] {s : Set α} {a : α} (h : a s) :
nhdsWithin a s = Filter.map Subtype.val (nhds a, h)
theorem mem_nhds_subtype_iff_nhdsWithin {α : Type u_1} [TopologicalSpace α] {s : Set α} {a : s} {t : Set s} :
t nhds a Subtype.val '' t nhdsWithin (a) s
theorem preimage_coe_mem_nhds_subtype {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} {a : s} :
Subtype.val ⁻¹' t nhds a t nhdsWithin (a) s
theorem eventually_nhds_subtype_iff {α : Type u_1} [TopologicalSpace α] (s : Set α) (a : s) (P : αProp) :
(∀ᶠ (x : s) in nhds a, P x) ∀ᶠ (x : α) in nhdsWithin (a) s, P x
theorem frequently_nhds_subtype_iff {α : Type u_1} [TopologicalSpace α] (s : Set α) (a : s) (P : αProp) :
(∃ᶠ (x : s) in nhds a, P x) ∃ᶠ (x : α) in nhdsWithin (a) s, P x
theorem tendsto_nhdsWithin_iff_subtype {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {s : Set α} {a : α} (h : a s) (f : αβ) (l : Filter β) :
Filter.Tendsto f (nhdsWithin a s) l Filter.Tendsto (s.restrict f) (nhds a, h) l
theorem ContinuousWithinAt.tendsto {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {x : α} (h : ContinuousWithinAt f s 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 Filter.Tendsto.comp as ContinuousWithinAt.comp will have a different meaning.

theorem ContinuousOn.continuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {x : α} (hf : ContinuousOn f s) (hx : x s) :
theorem continuousWithinAt_univ {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : αβ) (x : α) :
theorem continuous_iff_continuousOn_univ {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} :
theorem continuousWithinAt_iff_continuousAt_restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : αβ) {x : α} {s : Set α} (h : x s) :
ContinuousWithinAt f s x ContinuousAt (s.restrict f) x, h
theorem ContinuousWithinAt.tendsto_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {x : α} {s : Set α} {t : Set β} (h : ContinuousWithinAt f s x) (ht : Set.MapsTo f s t) :
theorem ContinuousWithinAt.tendsto_nhdsWithin_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {x : α} {s : Set α} (h : ContinuousWithinAt f s x) :
Filter.Tendsto f (nhdsWithin x s) (nhdsWithin (f x) (f '' s))
theorem ContinuousWithinAt.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {f : αγ} {g : βδ} {s : Set α} {t : Set β} {x : α} {y : β} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g t y) :
ContinuousWithinAt (Prod.map f g) (s ×ˢ t) (x, y)
theorem continuousWithinAt_prod_of_discrete_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology α] {f : α × βγ} {s : Set (α × β)} {x : α × β} :
ContinuousWithinAt f s x ContinuousWithinAt (fun (x_1 : β) => f (x.1, x_1)) {b : β | (x.1, b) s} x.2
theorem continuousWithinAt_prod_of_discrete_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology β] {f : α × βγ} {s : Set (α × β)} {x : α × β} :
ContinuousWithinAt f s x ContinuousWithinAt (fun (x_1 : α) => f (x_1, x.2)) {a : α | (a, x.2) s} x.1
theorem continuousAt_prod_of_discrete_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology α] {f : α × βγ} {x : α × β} :
ContinuousAt f x ContinuousAt (fun (x_1 : β) => f (x.1, x_1)) x.2
theorem continuousAt_prod_of_discrete_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology β] {f : α × βγ} {x : α × β} :
ContinuousAt f x ContinuousAt (fun (x_1 : α) => f (x_1, x.2)) x.1
theorem continuousOn_prod_of_discrete_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology α] {f : α × βγ} {s : Set (α × β)} :
ContinuousOn f s ∀ (a : α), ContinuousOn (fun (x : β) => f (a, x)) {b : β | (a, b) s}
theorem continuousOn_prod_of_discrete_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology β] {f : α × βγ} {s : Set (α × β)} :
ContinuousOn f s ∀ (b : β), ContinuousOn (fun (x : α) => f (x, b)) {a : α | (a, b) s}
theorem continuous_prod_of_discrete_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology α] {f : α × βγ} :
Continuous f ∀ (a : α), Continuous fun (x : β) => f (a, x)

If a function f a b is such that y ↦ f a b is continuous for all a, and a lives in a discrete space, then f is continuous, and vice versa.

theorem continuous_prod_of_discrete_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology β] {f : α × βγ} :
Continuous f ∀ (b : β), Continuous fun (x : α) => f (x, b)
theorem isOpenMap_prod_of_discrete_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology α] {f : α × βγ} :
IsOpenMap f ∀ (a : α), IsOpenMap fun (x : β) => f (a, x)
theorem isOpenMap_prod_of_discrete_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [DiscreteTopology β] {f : α × βγ} :
IsOpenMap f ∀ (b : β), IsOpenMap fun (x : α) => f (x, b)
theorem continuousWithinAt_pi {α : Type u_1} [TopologicalSpace α] {ι : Type u_5} {π : ιType u_6} [(i : ι) → TopologicalSpace (π i)] {f : α(i : ι) → π i} {s : Set α} {x : α} :
ContinuousWithinAt f s x ∀ (i : ι), ContinuousWithinAt (fun (y : α) => f y i) s x
theorem continuousOn_pi {α : Type u_1} [TopologicalSpace α] {ι : Type u_5} {π : ιType u_6} [(i : ι) → TopologicalSpace (π i)] {f : α(i : ι) → π i} {s : Set α} :
ContinuousOn f s ∀ (i : ι), ContinuousOn (fun (y : α) => f y i) s
theorem continuousOn_pi' {α : Type u_1} [TopologicalSpace α] {ι : Type u_5} {π : ιType u_6} [(i : ι) → TopologicalSpace (π i)] {f : α(i : ι) → π i} {s : Set α} (hf : ∀ (i : ι), ContinuousOn (fun (y : α) => f y i) s) :
theorem ContinuousWithinAt.fin_insertNth {α : Type u_1} [TopologicalSpace α] {n : } {π : Fin (n + 1)Type u_5} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : απ i} {a : α} {s : Set α} (hf : ContinuousWithinAt f s a) {g : α(j : Fin n) → π (i.succAbove j)} (hg : ContinuousWithinAt g s a) :
ContinuousWithinAt (fun (a : α) => i.insertNth (f a) (g a)) s a
theorem ContinuousOn.fin_insertNth {α : Type u_1} [TopologicalSpace α] {n : } {π : Fin (n + 1)Type u_5} [(i : Fin (n + 1)) → TopologicalSpace (π i)] (i : Fin (n + 1)) {f : απ i} {s : Set α} (hf : ContinuousOn f s) {g : α(j : Fin n) → π (i.succAbove j)} (hg : ContinuousOn g s) :
ContinuousOn (fun (a : α) => i.insertNth (f a) (g a)) s
theorem continuousOn_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} :
ContinuousOn f s xs, ∀ (t : Set β), IsOpen tf x t∃ (u : Set α), IsOpen u x u u s f ⁻¹' t
theorem continuousOn_iff_continuous_restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} :
ContinuousOn f s Continuous (s.restrict f)
theorem ContinuousOn.restrict {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} :
ContinuousOn f sContinuous (s.restrict f)

Alias of the forward direction of continuousOn_iff_continuous_restrict.

theorem ContinuousOn.restrict_mapsTo {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {t : Set β} (hf : ContinuousOn f s) (ht : Set.MapsTo f s t) :
theorem continuousOn_iff' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} :
ContinuousOn f s ∀ (t : Set β), IsOpen t∃ (u : Set α), IsOpen u f ⁻¹' t s = u s
theorem ContinuousOn.mono_dom {α : Type u_5} {β : Type u_6} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} (h₁ : t₂ t₁) {s : Set α} {f : αβ} (h₂ : ContinuousOn 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 ContinuousOn.mono_rng {α : Type u_5} {β : Type u_6} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β} {t₃ : TopologicalSpace β} (h₁ : t₂ t₃) {s : Set α} {f : αβ} (h₂ : ContinuousOn 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 continuousOn_iff_isClosed {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} :
ContinuousOn f s ∀ (t : Set β), IsClosed t∃ (u : Set α), IsClosed u f ⁻¹' t s = u s
theorem ContinuousOn.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {f : αγ} {g : βδ} {s : Set α} {t : Set β} (hf : ContinuousOn f s) (hg : ContinuousOn g t) :
theorem continuous_of_cover_nhds {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {ι : Sort u_5} {f : αβ} {s : ιSet α} (hs : ∀ (x : α), ∃ (i : ι), s i nhds x) (hf : ∀ (i : ι), ContinuousOn f (s i)) :
theorem continuousOn_empty {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : αβ) :
@[simp]
theorem continuousOn_singleton {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : αβ) (a : α) :
theorem Set.Subsingleton.continuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} (hs : s.Subsingleton) (f : αβ) :
theorem nhdsWithin_le_comap {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {x : α} {s : Set α} {f : αβ} (ctsf : ContinuousWithinAt f s x) :
@[simp]
theorem comap_nhdsWithin_range {β : Type u_2} [TopologicalSpace β] {α : Type u_5} (f : αβ) (y : β) :
theorem ContinuousWithinAt.mono {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {t : Set α} {x : α} (h : ContinuousWithinAt f t x) (hs : s t) :
theorem ContinuousWithinAt.mono_of_mem {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {t : Set α} {x : α} (h : ContinuousWithinAt f t x) (hs : t nhdsWithin x s) :
theorem continuousWithinAt_congr_nhds {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {t : Set α} {x : α} (h : nhdsWithin x s = nhdsWithin x t) :
theorem continuousWithinAt_inter' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {t : Set α} {x : α} (h : t nhdsWithin x s) :
theorem continuousWithinAt_inter {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {t : Set α} {x : α} (h : t nhds x) :
theorem continuousWithinAt_union {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {t : Set α} {x : α} :
theorem ContinuousWithinAt.union {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {t : Set α} {x : α} (hs : ContinuousWithinAt f s x) (ht : ContinuousWithinAt f t x) :
theorem ContinuousWithinAt.mem_closure_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) (hx : x closure s) :
f x closure (f '' s)
theorem ContinuousWithinAt.mem_closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {x : α} {A : Set β} (h : ContinuousWithinAt f s x) (hx : x closure s) (hA : Set.MapsTo f s A) :
f x closure A
theorem Set.MapsTo.closure_of_continuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {t : Set β} (h : Set.MapsTo f s t) (hc : xclosure s, ContinuousWithinAt f s x) :
theorem Set.MapsTo.closure_of_continuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {t : Set β} (h : Set.MapsTo f s t) (hc : ContinuousOn f (closure s)) :
theorem ContinuousWithinAt.image_closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} (hf : xclosure s, ContinuousWithinAt f s x) :
f '' closure s closure (f '' s)
theorem ContinuousOn.image_closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} (hf : ContinuousOn f (closure s)) :
f '' closure s closure (f '' s)
@[simp]
theorem continuousWithinAt_singleton {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {x : α} :
@[simp]
theorem continuousWithinAt_insert_self {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {x : α} {s : Set α} :
theorem ContinuousWithinAt.insert_self {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {x : α} {s : Set α} :

Alias of the reverse direction of continuousWithinAt_insert_self.

theorem ContinuousWithinAt.diff_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {t : Set α} {x : α} (ht : ContinuousWithinAt f t x) :
@[simp]
theorem continuousWithinAt_diff_self {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {x : α} :
@[simp]
theorem continuousWithinAt_compl_self {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {a : α} :
@[simp]
theorem continuousWithinAt_update_same {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [DecidableEq α] {f : αβ} {s : Set α} {x : α} {y : β} :
@[simp]
theorem continuousAt_update_same {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [DecidableEq α] {f : αβ} {x : α} {y : β} :
theorem IsOpenMap.continuousOn_image_of_leftInvOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} (h : IsOpenMap (s.restrict f)) {finv : βα} (hleft : Set.LeftInvOn finv f s) :
ContinuousOn finv (f '' s)
theorem IsOpenMap.continuousOn_range_of_leftInverse {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (hf : IsOpenMap f) {finv : βα} (hleft : Function.LeftInverse finv f) :
theorem ContinuousOn.congr_mono {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {g : αβ} {s : Set α} {s₁ : Set α} (h : ContinuousOn f s) (h' : Set.EqOn g f s₁) (h₁ : s₁ s) :
theorem ContinuousOn.congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {g : αβ} {s : Set α} (h : ContinuousOn f s) (h' : Set.EqOn g f s) :
theorem continuousOn_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {g : αβ} {s : Set α} (h' : Set.EqOn g f s) :
theorem ContinuousAt.continuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {x : α} (h : ContinuousAt f x) :
theorem continuousWithinAt_iff_continuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {x : α} (h : s nhds x) :
theorem ContinuousWithinAt.continuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) (hs : s nhds x) :
theorem IsOpen.continuousOn_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} (hs : IsOpen s) :
ContinuousOn f s ∀ ⦃a : α⦄, a sContinuousAt f a
theorem ContinuousOn.continuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {x : α} (h : ContinuousOn f s) (hx : s nhds x) :
theorem ContinuousAt.continuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} (hcont : xs, ContinuousAt f x) :
theorem ContinuousWithinAt.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : βγ} {f : αβ} {s : Set α} {t : Set β} {x : α} (hg : ContinuousWithinAt g t (f x)) (hf : ContinuousWithinAt f s x) (h : Set.MapsTo f s t) :
theorem ContinuousWithinAt.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : βγ} {f : αβ} {s : Set α} {t : Set β} {x : α} (hg : ContinuousWithinAt g t (f x)) (hf : ContinuousWithinAt f s x) :
theorem ContinuousAt.comp_continuousWithinAt {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : βγ} {f : αβ} {s : Set α} {x : α} (hg : ContinuousAt g (f x)) (hf : ContinuousWithinAt f s x) :
theorem ContinuousOn.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : βγ} {f : αβ} {s : Set α} {t : Set β} (hg : ContinuousOn g t) (hf : ContinuousOn f s) (h : Set.MapsTo f s t) :
theorem ContinuousOn.comp'' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : βγ} {f : αβ} {s : Set α} {t : Set β} (hg : ContinuousOn g t) (hf : ContinuousOn f s) (h : Set.MapsTo f s t) :
ContinuousOn (fun (x : α) => g (f x)) s
theorem ContinuousOn.mono {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {t : Set α} (hf : ContinuousOn f s) (h : t s) :
theorem antitone_continuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} :
theorem ContinuousOn.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : βγ} {f : αβ} {s : Set α} {t : Set β} (hg : ContinuousOn g t) (hf : ContinuousOn f s) :
ContinuousOn (g f) (s f ⁻¹' t)
theorem Continuous.continuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} (h : Continuous f) :
theorem Continuous.continuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {x : α} (h : Continuous f) :
theorem Continuous.comp_continuousOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : βγ} {f : αβ} {s : Set α} (hg : Continuous g) (hf : ContinuousOn f s) :
theorem Continuous.comp_continuousOn' {α : Type u_5} {β : Type u_6} {γ : Type u_7} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : βγ} {f : αβ} {s : Set α} (hg : Continuous g) (hf : ContinuousOn f s) :
ContinuousOn (fun (x : α) => g (f x)) s
theorem ContinuousOn.comp_continuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : βγ} {f : αβ} {s : Set β} (hg : ContinuousOn g s) (hf : Continuous f) (hs : ∀ (x : α), f x s) :
theorem continuousOn_apply {ι : Type u_5} {π : ιType u_6} [(i : ι) → TopologicalSpace (π i)] (i : ι) (s : Set ((i : ι) → π i)) :
ContinuousOn (fun (p : (i : ι) → π i) => p i) s
theorem ContinuousWithinAt.preimage_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {x : α} {s : Set α} {t : Set β} (h : ContinuousWithinAt f s x) (ht : t nhds (f x)) :
theorem Set.LeftInvOn.map_nhdsWithin_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {g : βα} {x : β} {s : Set β} (h : Set.LeftInvOn f g s) (hx : f (g x) = x) (hf : ContinuousWithinAt f (g '' s) (g x)) (hg : ContinuousWithinAt g s x) :
Filter.map g (nhdsWithin x s) = nhdsWithin (g x) (g '' s)
theorem Function.LeftInverse.map_nhds_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {g : βα} {x : β} (h : Function.LeftInverse f g) (hf : ContinuousWithinAt f (Set.range g) (g x)) (hg : ContinuousAt g x) :
theorem ContinuousWithinAt.preimage_mem_nhdsWithin' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {x : α} {s : Set α} {t : Set β} (h : ContinuousWithinAt f s x) (ht : t nhdsWithin (f x) (f '' s)) :
theorem ContinuousWithinAt.preimage_mem_nhdsWithin'' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {x : α} {y : β} {s : Set β} {t : Set β} (h : ContinuousWithinAt f (f ⁻¹' s) x) (ht : t nhdsWithin y s) (hxy : y = f x) :
theorem Filter.EventuallyEq.congr_continuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {g : αβ} {s : Set α} {x : α} (h : f =ᶠ[nhdsWithin x s] g) (hx : f x = g x) :
theorem ContinuousWithinAt.congr_of_eventuallyEq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {f₁ : αβ} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) (h₁ : f₁ =ᶠ[nhdsWithin x s] f) (hx : f₁ x = f x) :
theorem ContinuousWithinAt.congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {f₁ : αβ} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) (h₁ : ys, f₁ y = f y) (hx : f₁ x = f x) :
theorem ContinuousWithinAt.congr_mono {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {g : αβ} {s : Set α} {s₁ : Set α} {x : α} (h : ContinuousWithinAt f s x) (h' : Set.EqOn g f s₁) (h₁ : s₁ s) (hx : g x = f x) :
theorem continuousOn_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {c : β} :
ContinuousOn (fun (x : α) => c) s
theorem continuousWithinAt_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {b : β} {s : Set α} {x : α} :
ContinuousWithinAt (fun (x : α) => b) s x
theorem continuousOn_id {α : Type u_1} [TopologicalSpace α] {s : Set α} :
theorem continuousOn_id' {α : Type u_1} [TopologicalSpace α] (s : Set α) :
ContinuousOn (fun (x : α) => x) s
theorem continuousWithinAt_id {α : Type u_1} [TopologicalSpace α] {s : Set α} {x : α} :
theorem continuousOn_open_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} (hs : IsOpen s) :
ContinuousOn f s ∀ (t : Set β), IsOpen tIsOpen (s f ⁻¹' t)
theorem ContinuousOn.isOpen_inter_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {t : Set β} (hf : ContinuousOn f s) (hs : IsOpen s) (ht : IsOpen t) :
IsOpen (s f ⁻¹' t)
theorem ContinuousOn.isOpen_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {t : Set β} (h : ContinuousOn f s) (hs : IsOpen s) (hp : f ⁻¹' t s) (ht : IsOpen t) :
theorem ContinuousOn.preimage_isClosed_of_isClosed {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {t : Set β} (hf : ContinuousOn f s) (hs : IsClosed s) (ht : IsClosed t) :
theorem ContinuousOn.preimage_interior_subset_interior_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {t : Set β} (hf : ContinuousOn f s) (hs : IsOpen s) :
theorem continuousOn_of_locally_continuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} (h : xs, ∃ (t : Set α), IsOpen t x t ContinuousOn f (s t)) :
theorem continuousOn_to_generateFrom_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {s : Set α} {T : Set (Set β)} {f : αβ} :
ContinuousOn f s xs, tT, f x tf ⁻¹' t nhdsWithin x s
theorem continuousOn_isOpen_of_generateFrom {α : Type u_1} [TopologicalSpace α] {β : Type u_5} {s : Set α} {T : Set (Set β)} {f : αβ} (h : tT, IsOpen (s f ⁻¹' t)) :
theorem ContinuousWithinAt.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : αβ} {g : αγ} {s : Set α} {x : α} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
ContinuousWithinAt (fun (x : α) => (f x, g x)) s x
theorem ContinuousOn.prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : αβ} {g : αγ} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
ContinuousOn (fun (x : α) => (f x, g x)) s
theorem ContinuousAt.comp₂_continuousWithinAt {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {f : β × γδ} {g : αβ} {h : αγ} {x : α} {s : Set α} (hf : ContinuousAt f (g x, h x)) (hg : ContinuousWithinAt g s x) (hh : ContinuousWithinAt h s x) :
ContinuousWithinAt (fun (x : α) => f (g x, h x)) s x
theorem ContinuousAt.comp₂_continuousWithinAt_of_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {f : β × γδ} {g : αβ} {h : αγ} {x : α} {s : Set α} {y : β × γ} (hf : ContinuousAt f y) (hg : ContinuousWithinAt g s x) (hh : ContinuousWithinAt h s x) (e : (g x, h x) = y) :
ContinuousWithinAt (fun (x : α) => f (g x, h x)) s x
theorem Inducing.continuousWithinAt_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : αβ} {g : βγ} (hg : Inducing g) {s : Set α} {x : α} :
theorem Inducing.continuousOn_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : αβ} {g : βγ} (hg : Inducing g) {s : Set α} :
theorem Embedding.continuousOn_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : αβ} {g : βγ} (hg : Embedding g) {s : Set α} :
theorem Embedding.map_nhdsWithin_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (hf : Embedding f) (s : Set α) (x : α) :
Filter.map f (nhdsWithin x s) = nhdsWithin (f x) (f '' s)
theorem OpenEmbedding.map_nhdsWithin_preimage_eq {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} (hf : OpenEmbedding f) (s : Set β) (x : α) :
theorem continuousWithinAt_of_not_mem_closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} {x : α} (hx : xclosure s) :
theorem ContinuousOn.if' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {p : αProp} {f : αβ} {g : αβ} [(a : α) → Decidable (p a)] (hpf : as frontier {a : α | p a}, Filter.Tendsto f (nhdsWithin a (s {a : α | p a})) (nhds (if p a then f a else g a))) (hpg : as frontier {a : α | p a}, Filter.Tendsto g (nhdsWithin a (s {a : α | ¬p a})) (nhds (if p a then f a else g a))) (hf : ContinuousOn f (s {a : α | p a})) (hg : ContinuousOn g (s {a : α | ¬p a})) :
ContinuousOn (fun (a : α) => if p a then f a else g a) s
theorem ContinuousOn.piecewise' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set α} {f : αβ} {g : αβ} [(a : α) → Decidable (a t)] (hpf : as frontier t, Filter.Tendsto f (nhdsWithin a (s t)) (nhds (t.piecewise f g a))) (hpg : as frontier t, Filter.Tendsto g (nhdsWithin a (s t)) (nhds (t.piecewise f g a))) (hf : ContinuousOn f (s t)) (hg : ContinuousOn g (s t)) :
ContinuousOn (t.piecewise f g) s
theorem ContinuousOn.if {α : Type u_5} {β : Type u_6} [TopologicalSpace α] [TopologicalSpace β] {p : αProp} [(a : α) → Decidable (p a)] {s : Set α} {f : αβ} {g : αβ} (hp : as frontier {a : α | p a}, f a = g a) (hf : ContinuousOn f (s closure {a : α | p a})) (hg : ContinuousOn g (s closure {a : α | ¬p a})) :
ContinuousOn (fun (a : α) => if p a then f a else g a) s
theorem ContinuousOn.piecewise {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set α} {f : αβ} {g : αβ} [(a : α) → Decidable (a t)] (ht : as frontier t, f a = g a) (hf : ContinuousOn f (s closure t)) (hg : ContinuousOn g (s closure t)) :
ContinuousOn (t.piecewise f g) s
theorem continuous_if' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {p : αProp} {f : αβ} {g : αβ} [(a : α) → Decidable (p a)] (hpf : afrontier {x : α | p x}, Filter.Tendsto f (nhdsWithin a {x : α | p x}) (nhds (if p a then f a else g a))) (hpg : afrontier {x : α | p x}, Filter.Tendsto g (nhdsWithin a {x : α | ¬p x}) (nhds (if p a then f a else g a))) (hf : ContinuousOn f {x : α | p x}) (hg : ContinuousOn g {x : α | ¬p x}) :
Continuous fun (a : α) => if p a then f a else g a
theorem continuous_if {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {p : αProp} {f : αβ} {g : αβ} [(a : α) → Decidable (p a)] (hp : afrontier {x : α | p x}, f a = g a) (hf : ContinuousOn f (closure {x : α | p x})) (hg : ContinuousOn g (closure {x : α | ¬p x})) :
Continuous fun (a : α) => if p a then f a else g a
theorem Continuous.if {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {p : αProp} {f : αβ} {g : αβ} [(a : α) → Decidable (p a)] (hp : afrontier {x : α | p x}, f a = g a) (hf : Continuous f) (hg : Continuous g) :
Continuous fun (a : α) => if p a then f a else g a
theorem continuous_if_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (p : Prop) {f : αβ} {g : αβ} [Decidable p] (hf : pContinuous f) (hg : ¬pContinuous g) :
Continuous fun (a : α) => if p then f a else g a
theorem Continuous.if_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (p : Prop) {f : αβ} {g : αβ} [Decidable p] (hf : Continuous f) (hg : Continuous g) :
Continuous fun (a : α) => if p then f a else g a
theorem continuous_piecewise {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : αβ} {g : αβ} [(a : α) → Decidable (a s)] (hs : afrontier s, f a = g a) (hf : ContinuousOn f (closure s)) (hg : ContinuousOn g (closure s)) :
Continuous (s.piecewise f g)
theorem Continuous.piecewise {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {f : αβ} {g : αβ} [(a : α) → Decidable (a s)] (hs : afrontier s, f a = g a) (hf : Continuous f) (hg : Continuous g) :
Continuous (s.piecewise f g)
theorem continuous_indicator {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {f : αβ} {s : Set α} (hs : afrontier s, f a = 0) (hf : ContinuousOn f (closure s)) :
Continuous (s.indicator f)
theorem continuous_mulIndicator {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [One β] {f : αβ} {s : Set α} (hs : afrontier s, f a = 1) (hf : ContinuousOn f (closure s)) :
Continuous (s.mulIndicator f)
theorem Continuous.indicator {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [Zero β] {f : αβ} {s : Set α} (hs : afrontier s, f a = 0) (hf : Continuous f) :
Continuous (s.indicator f)
theorem Continuous.mulIndicator {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [One β] {f : αβ} {s : Set α} (hs : afrontier s, f a = 1) (hf : Continuous f) :
Continuous (s.mulIndicator f)
theorem IsOpen.ite' {α : Type u_1} [TopologicalSpace α] {s : Set α} {s' : Set α} {t : Set α} (hs : IsOpen s) (hs' : IsOpen s') (ht : xfrontier t, x s x s') :
IsOpen (t.ite s s')
theorem IsOpen.ite {α : Type u_1} [TopologicalSpace α] {s : Set α} {s' : Set α} {t : Set α} (hs : IsOpen s) (hs' : IsOpen s') (ht : s frontier t = s' frontier t) :
IsOpen (t.ite s s')
theorem ite_inter_closure_eq_of_inter_frontier_eq {α : Type u_1} [TopologicalSpace α] {s : Set α} {s' : Set α} {t : Set α} (ht : s frontier t = s' frontier t) :
t.ite s s' closure t = s closure t
theorem ite_inter_closure_compl_eq_of_inter_frontier_eq {α : Type u_1} [TopologicalSpace α] {s : Set α} {s' : Set α} {t : Set α} (ht : s frontier t = s' frontier t) :
t.ite s s' closure t = s' closure t
theorem continuousOn_piecewise_ite' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {s' : Set α} {t : Set α} {f : αβ} {f' : αβ} [(x : α) → Decidable (x t)] (h : ContinuousOn f (s closure t)) (h' : ContinuousOn f' (s' closure t)) (H : s frontier t = s' frontier t) (Heq : Set.EqOn f f' (s frontier t)) :
ContinuousOn (t.piecewise f f') (t.ite s s')
theorem continuousOn_piecewise_ite {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {s' : Set α} {t : Set α} {f : αβ} {f' : αβ} [(x : α) → Decidable (x t)] (h : ContinuousOn f s) (h' : ContinuousOn f' s') (H : s frontier t = s' frontier t) (Heq : Set.EqOn f f' (s frontier t)) :
ContinuousOn (t.piecewise f f') (t.ite s s')
theorem frontier_inter_open_inter {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} (ht : IsOpen t) :
theorem continuousOn_fst {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set (α × β)} :
ContinuousOn Prod.fst s
theorem continuousWithinAt_fst {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set (α × β)} {p : α × β} :
ContinuousWithinAt Prod.fst s p
theorem ContinuousOn.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : αβ × γ} {s : Set α} (hf : ContinuousOn f s) :
ContinuousOn (fun (x : α) => (f x).1) s
theorem ContinuousWithinAt.fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : αβ × γ} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) :
ContinuousWithinAt (fun (x : α) => (f x).1) s a
theorem continuousOn_snd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set (α × β)} :
ContinuousOn Prod.snd s
theorem continuousWithinAt_snd {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set (α × β)} {p : α × β} :
ContinuousWithinAt Prod.snd s p
theorem ContinuousOn.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : αβ × γ} {s : Set α} (hf : ContinuousOn f s) :
ContinuousOn (fun (x : α) => (f x).2) s
theorem ContinuousWithinAt.snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : αβ × γ} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) :
ContinuousWithinAt (fun (x : α) => (f x).2) s a
theorem continuousWithinAt_prod_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : αβ × γ} {s : Set α} {x : α} :
ContinuousWithinAt f s x ContinuousWithinAt (Prod.fst f) s x ContinuousWithinAt (Prod.snd f) s x