Continuity in topological spaces

For topological spaces X and Y, a function f : X → Y and a point x : X, ContinuousAt f x means f is continuous at x, and global continuity is Continuous f. There is also a version of continuity PContinuous for partially defined functions.

Tags

continuity, continuous function

theorem continuous_def {X : Type u_1} {Y : Type u_2} {x✝ : TopologicalSpace X} {x✝¹ : TopologicalSpace Y} {f : X → Y} : Continuous f ↔ ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)

theorem IsOpen.preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) {t : Set Y} (h : IsOpen t) : IsOpen (f ⁻¹' t)

theorem Equiv.continuous_symm_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) : Continuous ⇑e.symm ↔ IsOpenMap ⇑e

theorem Equiv.isOpenMap_symm_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ Y) : IsOpenMap ⇑e.symm ↔ Continuous ⇑e

theorem continuous_congr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : X → Y} (h : ∀ (x : X), f x = g x) : Continuous f ↔ Continuous g

theorem Continuous.congr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : X → Y} (h : Continuous f) (h' : ∀ (x : X), f x = g x) : Continuous g

theorem ContinuousAt.tendsto {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} (h : ContinuousAt f x) : Filter.Tendsto f (nhds x) (nhds (f x))

theorem continuousAt_def {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} : ContinuousAt f x ↔ ∀ A ∈ nhds (f x), f ⁻¹' A ∈ nhds x

theorem continuousAt_congr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {g : X → Y} (h : f =ᶠ[nhds x] g) : ContinuousAt f x ↔ ContinuousAt g x

theorem ContinuousAt.congr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {g : X → Y} (hf : ContinuousAt f x) (h : f =ᶠ[nhds x] g) : ContinuousAt g x

theorem ContinuousAt.preimage_mem_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {t : Set Y} (h : ContinuousAt f x) (ht : t ∈ nhds (f x)) : f ⁻¹' t ∈ nhds x

theorem ContinuousAt.eventually_mem {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} (hf : ContinuousAt f x) {s : Set Y} (hs : s ∈ nhds (f x)) : ∀ᶠ (y : X) in nhds x, f y ∈ s

If f x ∈ s ∈ 𝓝 (f x) for continuous f, then f y ∈ s near x.

This is essentially Filter.Tendsto.eventually_mem, but infers in more cases when applied.

theorem not_continuousAt_of_tendsto {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {l₁ : Filter X} {l₂ : Filter Y} {x : X} (hf : Filter.Tendsto f l₁ l₂) [l₁.NeBot] (hl₁ : l₁ ≤ nhds x) (hl₂ : Disjoint (nhds (f x)) l₂) : ¬ContinuousAt f x

If a function f tends to somewhere other than 𝓝 (f x) at x, then f is not continuous at x

theorem ClusterPt.map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {lx : Filter X} {ly : Filter Y} (H : ClusterPt x lx) (hfc : ContinuousAt f x) (hf : Filter.Tendsto f lx ly) : ClusterPt (f x) ly

theorem preimage_interior_subset_interior_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {t : Set Y} (hf : Continuous f) : f ⁻¹' interior t ⊆ interior (f ⁻¹' t)

See also interior_preimage_subset_preimage_interior.

theorem continuous_id {X : Type u_1} [TopologicalSpace X] : Continuous id

theorem continuous_id' {X : Type u_1} [TopologicalSpace X] : Continuous fun (x : X) => x

theorem Continuous.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : Continuous g) (hf : Continuous f) : Continuous (g ∘ f)

theorem Continuous.comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : Continuous g) (hf : Continuous f) : Continuous fun (x : X) => g (f x)

theorem Continuous.iterate {X : Type u_1} [TopologicalSpace X] {f : X → X} (h : Continuous f) (n : ℕ) : Continuous f^[n]

theorem ContinuousAt.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {x : X} {g : Y → Z} (hg : ContinuousAt g (f x)) (hf : ContinuousAt f x) : ContinuousAt (g ∘ f) x

theorem ContinuousAt.comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Y → Z} {x : X} (hg : ContinuousAt g (f x)) (hf : ContinuousAt f x) : ContinuousAt (fun (x : X) => g (f x)) x

theorem ContinuousAt.comp_of_eq {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {x : X} {y : Y} {g : Y → Z} (hg : ContinuousAt g y) (hf : ContinuousAt f x) (hy : f x = y) : ContinuousAt (g ∘ f) x

See note [comp_of_eq lemmas]

theorem Continuous.tendsto {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) (x : X) : Filter.Tendsto f (nhds x) (nhds (f x))

theorem Continuous.tendsto' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) (x : X) (y : Y) (h : f x = y) : Filter.Tendsto f (nhds x) (nhds y)

A version of Continuous.tendsto that allows one to specify a simpler form of the limit. E.g., one can write continuous_exp.tendsto' 0 1 exp_zero.

theorem Continuous.continuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} (h : Continuous f) : ContinuousAt f x

theorem continuous_iff_continuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : Continuous f ↔ ∀ (x : X), ContinuousAt f x

theorem continuousAt_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} : ContinuousAt (fun (x : X) => y) x

theorem continuous_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {y : Y} : Continuous fun (x : X) => y

theorem Filter.EventuallyEq.continuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {y : Y} (h : f =ᶠ[nhds x] fun (x : X) => y) : ContinuousAt f x

theorem continuous_of_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (h : ∀ (x y : X), f x = f y) : Continuous f

theorem continuousAt_id {X : Type u_1} [TopologicalSpace X] {x : X} : ContinuousAt id x

theorem continuousAt_id' {X : Type u_1} [TopologicalSpace X] (y : X) : ContinuousAt (fun (x : X) => x) y

theorem ContinuousAt.iterate {X : Type u_1} [TopologicalSpace X] {x : X} {f : X → X} (hf : ContinuousAt f x) (hx : f x = x) (n : ℕ) : ContinuousAt f^[n] x

theorem continuous_iff_isClosed {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : Continuous f ↔ ∀ (s : Set Y), IsClosed s → IsClosed (f ⁻¹' s)

theorem IsClosed.preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) {t : Set Y} (h : IsClosed t) : IsClosed (f ⁻¹' t)

theorem mem_closure_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {x : X} (hf : ContinuousAt f x) (hx : x ∈ closure s) : f x ∈ closure (f '' s)

theorem Continuous.closure_preimage_subset {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) (t : Set Y) : closure (f ⁻¹' t) ⊆ f ⁻¹' closure t

theorem Continuous.frontier_preimage_subset {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) (t : Set Y) : frontier (f ⁻¹' t) ⊆ f ⁻¹' frontier t

theorem Set.MapsTo.closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {t : Set Y} (h : MapsTo f s t) (hc : Continuous f) : MapsTo f (closure s) (closure t)

If a continuous map f maps s to t, then it maps closure s to closure t.

theorem image_closure_subset_closure_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (h : Continuous f) : f '' closure s ⊆ closure (f '' s)

See also IsClosedMap.closure_image_eq_of_continuous.

theorem closure_image_closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (h : Continuous f) : closure (f '' closure s) = closure (f '' s)

theorem closure_subset_preimage_closure_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (h : Continuous f) : closure s ⊆ f ⁻¹' closure (f '' s)

theorem map_mem_closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {x : X} {t : Set Y} (hf : Continuous f) (hx : x ∈ closure s) (ht : Set.MapsTo f s t) : f x ∈ closure t

theorem Set.MapsTo.closure_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {t : Set Y} (h : MapsTo f s t) (hc : Continuous f) (ht : IsClosed t) : MapsTo f (closure s) t

If a continuous map f maps s to a closed set t, then it maps closure s to t.

theorem Filter.Tendsto.lift'_closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) {l : Filter X} {l' : Filter Y} (h : Tendsto f l l') : Tendsto f (l.lift' closure) (l'.lift' closure)

theorem tendsto_lift'_closure_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) (x : X) : Filter.Tendsto f ((nhds x).lift' closure) ((nhds (f x)).lift' closure)

Function with dense range

theorem Function.Surjective.denseRange {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {f : α → X} (hf : Surjective f) : DenseRange f

A surjective map has dense range.

theorem denseRange_id {X : Type u_1} [TopologicalSpace X] : DenseRange id

theorem denseRange_iff_closure_range {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {f : α → X} : DenseRange f ↔ closure (Set.range f) = Set.univ

theorem DenseRange.closure_range {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {f : α → X} (h : DenseRange f) : closure (Set.range f) = Set.univ

@[simp]

theorem denseRange_subtype_val {X : Type u_1} [TopologicalSpace X] {p : X → Prop} : DenseRange Subtype.val ↔ Dense {x : X | p x}

theorem Dense.denseRange_val {X : Type u_1} [TopologicalSpace X] {s : Set X} (h : Dense s) : DenseRange Subtype.val

theorem Continuous.range_subset_closure_image_dense {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf : Continuous f) (hs : Dense s) : Set.range f ⊆ closure (f '' s)

theorem DenseRange.dense_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf' : DenseRange f) (hf : Continuous f) (hs : Dense s) : Dense (f '' s)

The image of a dense set under a continuous map with dense range is a dense set.

theorem DenseRange.subset_closure_image_preimage_of_isOpen {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {f : α → X} {s : Set X} (hf : DenseRange f) (hs : IsOpen s) : s ⊆ closure (f '' (f ⁻¹' s))

If f has dense range and s is an open set in the codomain of f, then the image of the preimage of s under f is dense in s.

theorem DenseRange.dense_of_mapsTo {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf' : DenseRange f) (hf : Continuous f) (hs : Dense s) {t : Set Y} (ht : Set.MapsTo f s t) : Dense t

If a continuous map with dense range maps a dense set to a subset of t, then t is a dense set.

theorem DenseRange.comp {Y : Type u_2} {Z : Type u_3} [TopologicalSpace Y] [TopologicalSpace Z] {α : Type u_4} {g : Y → Z} {f : α → Y} (hg : DenseRange g) (hf : DenseRange f) (cg : Continuous g) : DenseRange (g ∘ f)

Composition of a continuous map with dense range and a function with dense range has dense range.

theorem DenseRange.nonempty_iff {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {f : α → X} (hf : DenseRange f) : Nonempty α ↔ Nonempty X

theorem DenseRange.nonempty {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {f : α → X} [h : Nonempty X] (hf : DenseRange f) : Nonempty α

noncomputable def DenseRange.some {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {f : α → X} (hf : DenseRange f) (x : X) : α

Given a function f : X → Y with dense range and y : Y, returns some x : X.

Equations

• hf.some x = Classical.choice ⋯

theorem DenseRange.exists_mem_open {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {f : α → X} {s : Set X} (hf : DenseRange f) (ho : IsOpen s) (hs : s.Nonempty) : ∃ (a : α), f a ∈ s

theorem DenseRange.mem_nhds {X : Type u_1} [TopologicalSpace X] {x : X} {α : Type u_4} {f : α → X} {s : Set X} (h : DenseRange f) (hs : s ∈ nhds x) : ∃ (a : α), f a ∈ s