doc-next-gen

Mathlib.Topology.Continuous

Module docstring

{"# 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 ","### Function with dense range "}

continuous_def theorem
{_ : TopologicalSpace X} {_ : TopologicalSpace Y} {f : X → Y} : Continuous f ↔ ∀ s, IsOpen s → IsOpen (f ⁻¹' s)
Full source 
theorem continuous_def {_ : TopologicalSpace X} {_ : TopologicalSpace Y} {f : X → Y} :
    ContinuousContinuous f ↔ ∀ s, IsOpen s → IsOpen (f ⁻¹' s) :=
  ⟨fun hf => hf.1, fun h => ⟨h⟩⟩
Characterization of Continuity via Open Sets
Informal description
Let $X$ and $Y$ be topological spaces and $f : X \to Y$ be a function. Then $f$ is continuous if and only if for every open set $s \subseteq Y$, the preimage $f^{-1}(s)$ is open in $X$.
IsOpen.preimage theorem
(hf : Continuous f) {t : Set Y} (h : IsOpen t) : IsOpen (f ⁻¹' t)
Full source 
theorem IsOpen.preimage (hf : Continuous f) {t : Set Y} (h : IsOpen t) :
    IsOpen (f ⁻¹' t) :=
  hf.isOpen_preimage t h
Preimage of Open Set Under Continuous Function is Open
Informal description
Let $X$ and $Y$ be topological spaces and $f : X \to Y$ be a continuous function. For any open set $t \subseteq Y$, the preimage $f^{-1}(t)$ is open in $X$.
Equiv.continuous_symm_iff theorem
(e : X ≃ Y) : Continuous e.symm ↔ IsOpenMap e
Full source 
lemma Equiv.continuous_symm_iff (e : X ≃ Y) : ContinuousContinuous e.symm ↔ IsOpenMap e := by
  simp_rw [continuous_def, ← Set.image_equiv_eq_preimage_symm, IsOpenMap]
Continuity of Inverse Equivalence vs Openness of Original Map
Informal description
For a bijective equivalence $e : X \simeq Y$ between topological spaces, the inverse map $e^{-1}$ is continuous if and only if the original map $e$ is an open map (i.e., maps open sets to open sets).
continuous_congr theorem
{g : X → Y} (h : ∀ x, f x = g x) : Continuous f ↔ Continuous g
Full source 
theorem continuous_congr {g : X → Y} (h : ∀ x, f x = g x) :
    ContinuousContinuous f ↔ Continuous g :=
  .of_eq <| congrArg _ <| funext h
Continuity is preserved under pointwise equality
Informal description
For two functions $f, g : X \to Y$ between topological spaces such that $f(x) = g(x)$ for all $x \in X$, the function $f$ is continuous if and only if $g$ is continuous.
Continuous.congr theorem
{g : X → Y} (h : Continuous f) (h' : ∀ x, f x = g x) : Continuous g
Full source 
theorem Continuous.congr {g : X → Y} (h : Continuous f) (h' : ∀ x, f x = g x) : Continuous g :=
  continuous_congr h' |>.mp h
Continuity Transfer via Pointwise Equality
Informal description
Let $f, g : X \to Y$ be functions between topological spaces. If $f$ is continuous and $f(x) = g(x)$ for all $x \in X$, then $g$ is continuous.
ContinuousAt.tendsto theorem
(h : ContinuousAt f x) : Tendsto f (𝓝 x) (𝓝 (f x))
Full source 
theorem ContinuousAt.tendsto (h : ContinuousAt f x) :
    Tendsto f (𝓝 x) (𝓝 (f x)) :=
  h
Continuity at a point implies limit equals function value
Informal description
If a function $f \colon X \to Y$ between topological spaces is continuous at a point $x \in X$, then the limit of $f$ at $x$ exists and equals $f(x)$, i.e., $f$ tends to $f(x)$ as the input tends to $x$.
continuousAt_def theorem
: ContinuousAt f x ↔ ∀ A ∈ 𝓝 (f x), f ⁻¹' A ∈ 𝓝 x
Full source 
theorem continuousAt_def : ContinuousAtContinuousAt f x ↔ ∀ A ∈ 𝓝 (f x), f ⁻¹' A ∈ 𝓝 x :=
  Iff.rfl
Neighborhood Characterization of Continuity at a Point
Informal description
A function $f : X \to Y$ between topological spaces is continuous at a point $x \in X$ if and only if for every neighborhood $A$ of $f(x)$ in $Y$, the preimage $f^{-1}(A)$ is a neighborhood of $x$ in $X$.
continuousAt_congr theorem
{g : X → Y} (h : f =ᶠ[𝓝 x] g) : ContinuousAt f x ↔ ContinuousAt g x
Full source 
theorem continuousAt_congr {g : X → Y} (h : f =ᶠ[𝓝 x] g) :
    ContinuousAtContinuousAt f x ↔ ContinuousAt g x := by
  simp only [ContinuousAt, tendsto_congr' h, h.eq_of_nhds]
Continuity at a Point is Local Property
Informal description
Let $X$ and $Y$ be topological spaces, and let $f, g : X \to Y$ be functions. If $f$ and $g$ are eventually equal in a neighborhood of $x \in X$ (i.e., $f(y) = g(y)$ for all $y$ in some neighborhood of $x$), then $f$ is continuous at $x$ if and only if $g$ is continuous at $x$.
ContinuousAt.congr theorem
{g : X → Y} (hf : ContinuousAt f x) (h : f =ᶠ[𝓝 x] g) : ContinuousAt g x
Full source 
theorem ContinuousAt.congr {g : X → Y} (hf : ContinuousAt f x) (h : f =ᶠ[𝓝 x] g) :
    ContinuousAt g x :=
  (continuousAt_congr h).1 hf
Continuity at a Point is Preserved under Local Equality
Informal description
Let $X$ and $Y$ be topological spaces, $f, g : X \to Y$ be functions, and $x \in X$. If $f$ is continuous at $x$ and $f$ is eventually equal to $g$ in a neighborhood of $x$ (i.e., $f(y) = g(y)$ for all $y$ in some neighborhood of $x$), then $g$ is also continuous at $x$.
ContinuousAt.preimage_mem_nhds theorem
{t : Set Y} (h : ContinuousAt f x) (ht : t ∈ 𝓝 (f x)) : f ⁻¹' t ∈ 𝓝 x
Full source 
theorem ContinuousAt.preimage_mem_nhds {t : Set Y} (h : ContinuousAt f x)
    (ht : t ∈ 𝓝 (f x)) : f ⁻¹' tf ⁻¹' t ∈ 𝓝 x :=
  h ht
Preimage of Neighborhood under Continuous Function is Neighborhood
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ be a function, and $x \in X$. If $f$ is continuous at $x$ and $t$ is a neighborhood of $f(x)$ in $Y$, then the preimage $f^{-1}(t)$ is a neighborhood of $x$ in $X$.
ContinuousAt.eventually_mem theorem
{f : X → Y} {x : X} (hf : ContinuousAt f x) {s : Set Y} (hs : s ∈ 𝓝 (f x)) : ∀ᶠ y in 𝓝 x, f y ∈ s
Full source 
/-- 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 ContinuousAt.eventually_mem {f : X → Y} {x : X} (hf : ContinuousAt f x) {s : Set Y}
    (hs : s ∈ 𝓝 (f x)) : ∀ᶠ y in 𝓝 x, f y ∈ s :=
  hf hs
Continuous functions map nearby points into neighborhoods
Informal description
Let $f : X \to Y$ be a function between topological spaces, continuous at a point $x \in X$. If $s$ is a neighborhood of $f(x)$ in $Y$, then for all $y$ sufficiently close to $x$, we have $f(y) \in s$.
not_continuousAt_of_tendsto theorem
{f : X → Y} {l₁ : Filter X} {l₂ : Filter Y} {x : X} (hf : Tendsto f l₁ l₂) [l₁.NeBot] (hl₁ : l₁ ≤ 𝓝 x) (hl₂ : Disjoint (𝓝 (f x)) l₂) : ¬ContinuousAt f x
Full source 
/-- If a function `f` tends to somewhere other than `𝓝 (f x)` at `x`,
then `f` is not continuous at `x`
-/
lemma not_continuousAt_of_tendsto {f : X → Y} {l₁ : Filter X} {l₂ : Filter Y} {x : X}
    (hf : Tendsto f l₁ l₂) [l₁.NeBot] (hl₁ : l₁ ≤ 𝓝 x) (hl₂ : Disjoint (𝓝 (f x)) l₂) :
    ¬ ContinuousAt f x := fun cont ↦
  (cont.mono_left hl₁).not_tendsto hl₂ hf
Non-continuity via Disjoint Filter Limits
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a function, and $x \in X$. Suppose there exist filters $l₁$ on $X$ and $l₂$ on $Y$ such that: 1. $f$ tends to $l₂$ along $l₁$, 2. $l₁$ is a nontrivial filter (i.e., $l₁$ is not the bottom filter), 3. $l₁$ is finer than the neighborhood filter of $x$ (i.e., $l₁ ≤ 𝓝 x$), and 4. The neighborhood filter of $f(x)$ is disjoint from $l₂$. Then $f$ is not continuous at $x$.
ClusterPt.map theorem
{lx : Filter X} {ly : Filter Y} (H : ClusterPt x lx) (hfc : ContinuousAt f x) (hf : Tendsto f lx ly) : ClusterPt (f x) ly
Full source 
theorem ClusterPt.map {lx : Filter X} {ly : Filter Y} (H : ClusterPt x lx)
    (hfc : ContinuousAt f x) (hf : Tendsto f lx ly) : ClusterPt (f x) ly :=
  (NeBot.map H f).mono <| hfc.tendsto.inf hf
Continuous Functions Preserve Cluster Points
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a function continuous at $x \in X$, and $lx$ a filter on $X$ such that $x$ is a cluster point of $lx$. If $f$ tends to $ly$ along $lx$, then $f(x)$ is a cluster point of $ly$.
preimage_interior_subset_interior_preimage theorem
{t : Set Y} (hf : Continuous f) : f ⁻¹' interior t ⊆ interior (f ⁻¹' t)
Full source 
/-- See also `interior_preimage_subset_preimage_interior`. -/
theorem preimage_interior_subset_interior_preimage {t : Set Y} (hf : Continuous f) :
    f ⁻¹' interior tf ⁻¹' interior t ⊆ interior (f ⁻¹' t) :=
  interior_maximal (preimage_mono interior_subset) (isOpen_interior.preimage hf)
Preimage of Interior is Subset of Interior of Preimage under Continuous Function
Informal description
Let $X$ and $Y$ be topological spaces and $f : X \to Y$ be a continuous function. For any subset $t \subseteq Y$, the preimage of the interior of $t$ under $f$ is contained in the interior of the preimage of $t$, i.e., $f^{-1}(\text{int}(t)) \subseteq \text{int}(f^{-1}(t))$.
continuous_id theorem
: Continuous (id : X → X)
Full source 
@[continuity]
theorem continuous_id : Continuous (id : X → X) :=
  continuous_def.2 fun _ => id
Continuity of the Identity Function
Informal description
The identity function $\text{id} : X \to X$ on a topological space $X$ is continuous.
continuous_id' theorem
: Continuous (fun (x : X) => x)
Full source 
@[continuity, fun_prop]
theorem continuous_id' : Continuous (fun (x : X) => x) := continuous_id
Continuity of the Identity Map
Informal description
The identity function $x \mapsto x$ on a topological space $X$ is continuous.
Continuous.comp theorem
{g : Y → Z} (hg : Continuous g) (hf : Continuous f) : Continuous (g ∘ f)
Full source 
theorem Continuous.comp {g : Y → Z} (hg : Continuous g) (hf : Continuous f) :
    Continuous (g ∘ f) :=
  continuous_def.2 fun _ h => (h.preimage hg).preimage hf
Continuity of Function Composition
Informal description
Let $X$, $Y$, and $Z$ be topological spaces, and let $f : X \to Y$ and $g : Y \to Z$ be continuous functions. Then the composition $g \circ f : X \to Z$ is continuous.
Continuous.comp' theorem
{g : Y → Z} (hg : Continuous g) (hf : Continuous f) : Continuous (fun x => g (f x))
Full source 
@[continuity, fun_prop]
theorem Continuous.comp' {g : Y → Z} (hg : Continuous g) (hf : Continuous f) :
    Continuous (fun x => g (f x)) := hg.comp hf
Continuity of Pointwise Composition of Continuous Functions
Informal description
Let $X$, $Y$, and $Z$ be topological spaces, and let $f : X \to Y$ and $g : Y \to Z$ be continuous functions. Then the function $x \mapsto g(f(x))$ is continuous.
Continuous.iterate theorem
{f : X → X} (h : Continuous f) (n : ℕ) : Continuous f^[n]
Full source 
theorem Continuous.iterate {f : X → X} (h : Continuous f) (n : ℕ) : Continuous f^[n] :=
  Nat.recOn n continuous_id fun _ ihn => ihn.comp h
Continuity of Iterated Function
Informal description
Let $X$ be a topological space and $f : X \to X$ a continuous function. Then for any natural number $n$, the $n$-th iterate $f^{[n]}$ of $f$ is also continuous.
ContinuousAt.comp theorem
{g : Y → Z} (hg : ContinuousAt g (f x)) (hf : ContinuousAt f x) : ContinuousAt (g ∘ f) x
Full source 
nonrec theorem ContinuousAt.comp {g : Y → Z} (hg : ContinuousAt g (f x))
    (hf : ContinuousAt f x) : ContinuousAt (g ∘ f) x :=
  hg.comp hf
Continuity of Composition at a Point
Informal description
Let $X$, $Y$, and $Z$ be topological spaces, and let $f : X \to Y$ and $g : Y \to Z$ be functions. If $f$ is continuous at a point $x \in X$ and $g$ is continuous at $f(x) \in Y$, then the composition $g \circ f$ is continuous at $x$.
ContinuousAt.comp' theorem
{g : Y → Z} {x : X} (hg : ContinuousAt g (f x)) (hf : ContinuousAt f x) : ContinuousAt (fun x => g (f x)) x
Full source 
@[fun_prop]
theorem ContinuousAt.comp' {g : Y → Z} {x : X} (hg : ContinuousAt g (f x))
    (hf : ContinuousAt f x) : ContinuousAt (fun x => g (f x)) x := ContinuousAt.comp hg hf
Continuity of Function Composition at a Point (Pointwise Form)
Informal description
Let $X$, $Y$, and $Z$ be topological spaces, and let $f : X \to Y$ and $g : Y \to Z$ be functions. If $f$ is continuous at a point $x \in X$ and $g$ is continuous at $f(x) \in Y$, then the function $x \mapsto g(f(x))$ is continuous at $x$.
ContinuousAt.comp_of_eq theorem
{g : Y → Z} (hg : ContinuousAt g y) (hf : ContinuousAt f x) (hy : f x = y) : ContinuousAt (g ∘ f) x
Full source 
/-- See note [comp_of_eq lemmas] -/
theorem ContinuousAt.comp_of_eq {g : Y → Z} (hg : ContinuousAt g y)
    (hf : ContinuousAt f x) (hy : f x = y) : ContinuousAt (g ∘ f) x := by subst hy; exact hg.comp hf
Continuity of Composition at a Point with Equality Condition
Informal description
Let $X$, $Y$, and $Z$ be topological spaces, and let $f : X \to Y$ and $g : Y \to Z$ be functions. If $g$ is continuous at a point $y \in Y$, $f$ is continuous at a point $x \in X$, and $f(x) = y$, then the composition $g \circ f$ is continuous at $x$.
Continuous.tendsto theorem
(hf : Continuous f) (x) : Tendsto f (𝓝 x) (𝓝 (f x))
Full source 
theorem Continuous.tendsto (hf : Continuous f) (x) : Tendsto f (𝓝 x) (𝓝 (f x)) :=
  ((nhds_basis_opens x).tendsto_iff <| nhds_basis_opens <| f x).2 fun t ⟨hxt, ht⟩ =>
    ⟨f ⁻¹' t, ⟨hxt, ht.preimage hf⟩, Subset.rfl⟩
Continuous Functions Preserve Limits of Neighborhoods
Informal description
Let $X$ and $Y$ be topological spaces and $f : X \to Y$ be a continuous function. For any point $x \in X$, the function $f$ maps neighborhoods of $x$ to neighborhoods of $f(x)$, i.e., $\lim_{y \to x} f(y) = f(x)$.
Continuous.tendsto' theorem
(hf : Continuous f) (x : X) (y : Y) (h : f x = y) : Tendsto f (𝓝 x) (𝓝 y)
Full source 
/-- 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.tendsto' (hf : Continuous f) (x : X) (y : Y) (h : f x = y) :
    Tendsto f (𝓝 x) (𝓝 y) :=
  h ▸ hf.tendsto x
Limit of Continuous Function at a Point with Specified Value
Informal description
Let $X$ and $Y$ be topological spaces and $f : X \to Y$ be a continuous function. For any point $x \in X$ and $y \in Y$ such that $f(x) = y$, the function $f$ maps neighborhoods of $x$ to neighborhoods of $y$, i.e., $\lim_{z \to x} f(z) = y$.
Continuous.continuousAt theorem
(h : Continuous f) : ContinuousAt f x
Full source 
@[fun_prop]
theorem Continuous.continuousAt (h : Continuous f) : ContinuousAt f x :=
  h.tendsto x
Global Continuity Implies Pointwise Continuity
Informal description
If a function $f : X \to Y$ between topological spaces is continuous, then it is continuous at every point $x \in X$.
continuous_iff_continuousAt theorem
: Continuous f ↔ ∀ x, ContinuousAt f x
Full source 
theorem continuous_iff_continuousAt : ContinuousContinuous f ↔ ∀ x, ContinuousAt f x :=
  ⟨Continuous.tendsto, fun hf => continuous_def.2 fun _U hU => isOpen_iff_mem_nhds.2 fun x hx =>
    hf x <| hU.mem_nhds hx⟩
Global Continuity is Equivalent to Pointwise Continuity
Informal description
A function $f : X \to Y$ between topological spaces is continuous if and only if it is continuous at every point $x \in X$.
continuousAt_const theorem
: ContinuousAt (fun _ : X => y) x
Full source 
@[fun_prop]
theorem continuousAt_const : ContinuousAt (fun _ : X => y) x :=
  tendsto_const_nhds
Continuity of Constant Functions at a Point
Informal description
For any topological spaces $X$ and $Y$, any point $x \in X$, and any constant function $f : X \to Y$ defined by $f(\_) = y$ for some fixed $y \in Y$, the function $f$ is continuous at $x$.
continuous_const theorem
: Continuous fun _ : X => y
Full source 
@[continuity, fun_prop]
theorem continuous_const : Continuous fun _ : X => y :=
  continuous_iff_continuousAt.mpr fun _ => continuousAt_const
Continuity of Constant Functions
Informal description
For any topological spaces $X$ and $Y$, the constant function $f : X \to Y$ defined by $f(x) = y$ for some fixed $y \in Y$ is continuous.
Filter.EventuallyEq.continuousAt theorem
(h : f =ᶠ[𝓝 x] fun _ => y) : ContinuousAt f x
Full source 
theorem Filter.EventuallyEq.continuousAt (h : f =ᶠ[𝓝 x] fun _ => y) :
    ContinuousAt f x :=
  (continuousAt_congr h).2 tendsto_const_nhds
Continuity at a Point for Eventually Constant Functions
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ be a function, and $x \in X$ be a point. If $f$ is eventually equal to a constant function $y$ in a neighborhood of $x$ (i.e., $f(z) = y$ for all $z$ in some neighborhood of $x$), then $f$ is continuous at $x$.
continuousAt_id theorem
: ContinuousAt id x
Full source 
theorem continuousAt_id : ContinuousAt id x :=
  continuous_id.continuousAt
Pointwise Continuity of the Identity Function
Informal description
The identity function $\text{id} : X \to X$ on a topological space $X$ is continuous at every point $x \in X$.
continuousAt_id' theorem
(y) : ContinuousAt (fun x : X => x) y
Full source 
@[fun_prop]
theorem continuousAt_id' (y) : ContinuousAt (fun x : X => x) y := continuousAt_id
Pointwise Continuity of the Identity Function (alternative form)
Informal description
For any point $y$ in a topological space $X$, the identity function $x \mapsto x$ is continuous at $y$.
ContinuousAt.iterate theorem
{f : X → X} (hf : ContinuousAt f x) (hx : f x = x) (n : ℕ) : ContinuousAt f^[n] x
Full source 
theorem ContinuousAt.iterate {f : X → X} (hf : ContinuousAt f x) (hx : f x = x) (n : ℕ) :
    ContinuousAt f^[n] x :=
  Nat.recOn n continuousAt_id fun _n ihn ↦ ihn.comp_of_eq hf hx
Continuity of Iterated Function at Fixed Point
Informal description
Let $X$ be a topological space, $f : X \to X$ a function continuous at a point $x \in X$, and suppose $f(x) = x$. Then for any natural number $n$, the $n$-th iterate $f^{[n]}$ is also continuous at $x$.
continuous_iff_isClosed theorem
: Continuous f ↔ ∀ s, IsClosed s → IsClosed (f ⁻¹' s)
Full source 
theorem continuous_iff_isClosed : ContinuousContinuous f ↔ ∀ s, IsClosed s → IsClosed (f ⁻¹' s) :=
  continuous_def.trans <| compl_surjective.forall.trans <| by
    simp only [isOpen_compl_iff, preimage_compl]
Characterization of Continuity via Closed Sets
Informal description
Let $X$ and $Y$ be topological spaces and $f : X \to Y$ be a function. Then $f$ is continuous if and only if for every closed set $s \subseteq Y$, the preimage $f^{-1}(s)$ is closed in $X$.
IsClosed.preimage theorem
(hf : Continuous f) {t : Set Y} (h : IsClosed t) : IsClosed (f ⁻¹' t)
Full source 
theorem IsClosed.preimage (hf : Continuous f) {t : Set Y} (h : IsClosed t) :
    IsClosed (f ⁻¹' t) :=
  continuous_iff_isClosed.mp hf t h
Preimage of Closed Set under Continuous Function is Closed
Informal description
Let $X$ and $Y$ be topological spaces and $f : X \to Y$ be a continuous function. For any closed set $t \subseteq Y$, the preimage $f^{-1}(t)$ is closed in $X$.
mem_closure_image theorem
(hf : ContinuousAt f x) (hx : x ∈ closure s) : f x ∈ closure (f '' s)
Full source 
theorem mem_closure_image (hf : ContinuousAt f x)
    (hx : x ∈ closure s) : f x ∈ closure (f '' s) :=
  mem_closure_of_frequently_of_tendsto
    ((mem_closure_iff_frequently.1 hx).mono fun _ => mem_image_of_mem _) hf
Image of Closure Point under Continuous Function Belongs to Closure of Image
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ be a function continuous at $x \in X$, and $s \subseteq X$ be a subset such that $x$ belongs to the closure of $s$. Then $f(x)$ belongs to the closure of the image $f(s)$ in $Y$.
Continuous.closure_preimage_subset theorem
(hf : Continuous f) (t : Set Y) : closure (f ⁻¹' t) ⊆ f ⁻¹' closure t
Full source 
theorem Continuous.closure_preimage_subset (hf : Continuous f) (t : Set Y) :
    closureclosure (f ⁻¹' t) ⊆ f ⁻¹' closure t := by
  rw [← (isClosed_closure.preimage hf).closure_eq]
  exact closure_mono (preimage_mono subset_closure)
Closure of Preimage is Contained in Preimage of Closure under Continuous Function
Informal description
Let $X$ and $Y$ be topological spaces and $f : X \to Y$ be a continuous function. For any subset $t \subseteq Y$, the closure of the preimage $f^{-1}(t)$ is contained in the preimage of the closure of $t$, i.e., $\overline{f^{-1}(t)} \subseteq f^{-1}(\overline{t})$.
Continuous.frontier_preimage_subset theorem
(hf : Continuous f) (t : Set Y) : frontier (f ⁻¹' t) ⊆ f ⁻¹' frontier t
Full source 
theorem Continuous.frontier_preimage_subset (hf : Continuous f) (t : Set Y) :
    frontierfrontier (f ⁻¹' t) ⊆ f ⁻¹' frontier t :=
  diff_subset_diff (hf.closure_preimage_subset t) (preimage_interior_subset_interior_preimage hf)
Frontier of Preimage is Contained in Preimage of Frontier under Continuous Function
Informal description
Let $X$ and $Y$ be topological spaces and $f : X \to Y$ be a continuous function. For any subset $t \subseteq Y$, the frontier of the preimage $f^{-1}(t)$ is contained in the preimage of the frontier of $t$, i.e., $\partial f^{-1}(t) \subseteq f^{-1}(\partial t)$.
Set.MapsTo.closure theorem
{t : Set Y} (h : MapsTo f s t) (hc : Continuous f) : MapsTo f (closure s) (closure t)
Full source 
/-- If a continuous map `f` maps `s` to `t`, then it maps `closure s` to `closure t`. -/
protected theorem Set.MapsTo.closure {t : Set Y} (h : MapsTo f s t)
    (hc : Continuous f) : MapsTo f (closure s) (closure t) := by
  simp only [MapsTo, mem_closure_iff_clusterPt]
  exact fun x hx => hx.map hc.continuousAt (tendsto_principal_principal.2 h)
Continuous Functions Preserve Closure Under Mapping
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a continuous function, and $s \subseteq X$, $t \subseteq Y$ subsets such that $f$ maps $s$ into $t$. Then $f$ maps the closure of $s$ into the closure of $t$.
image_closure_subset_closure_image theorem
(h : Continuous f) : f '' closure s ⊆ closure (f '' s)
Full source 
/-- See also `IsClosedMap.closure_image_eq_of_continuous`. -/
theorem image_closure_subset_closure_image (h : Continuous f) :
    f '' closure sf '' closure s ⊆ closure (f '' s) :=
  ((mapsTo_image f s).closure h).image_subset
Image of Closure is Contained in Closure of Image under Continuous Function
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a continuous function, and $s \subseteq X$ a subset. Then the image of the closure of $s$ under $f$ is contained in the closure of the image of $s$ under $f$, i.e., $$f(\overline{s}) \subseteq \overline{f(s)}.$$
closure_image_closure theorem
(h : Continuous f) : closure (f '' closure s) = closure (f '' s)
Full source 
theorem closure_image_closure (h : Continuous f) :
    closure (f '' closure s) = closure (f '' s) :=
  Subset.antisymm
    (closure_minimal (image_closure_subset_closure_image h) isClosed_closure)
    (closure_mono <| image_subset _ subset_closure)
Closure of Image of Closure Equals Closure of Image under Continuous Function
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a continuous function, and $s \subseteq X$ a subset. Then the closure of the image of the closure of $s$ under $f$ is equal to the closure of the image of $s$ under $f$, i.e., $$\overline{f(\overline{s})} = \overline{f(s)}.$$
closure_subset_preimage_closure_image theorem
(h : Continuous f) : closure s ⊆ f ⁻¹' closure (f '' s)
Full source 
theorem closure_subset_preimage_closure_image (h : Continuous f) :
    closureclosure s ⊆ f ⁻¹' closure (f '' s) :=
  (mapsTo_image _ _).closure h
Closure is Contained in Preimage of Image Closure under Continuous Function
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a continuous function, and $s \subseteq X$ a subset. Then the closure of $s$ is contained in the preimage under $f$ of the closure of the image of $s$ under $f$, i.e., $$\overline{s} \subseteq f^{-1}(\overline{f(s)}).$$
map_mem_closure theorem
{t : Set Y} (hf : Continuous f) (hx : x ∈ closure s) (ht : MapsTo f s t) : f x ∈ closure t
Full source 
theorem map_mem_closure {t : Set Y} (hf : Continuous f)
    (hx : x ∈ closure s) (ht : MapsTo f s t) : f x ∈ closure t :=
  ht.closure hf hx
Continuous Functions Preserve Closure Membership
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a continuous function, $s \subseteq X$ a subset, and $t \subseteq Y$ such that $f$ maps $s$ into $t$. If $x$ is in the closure of $s$, then $f(x)$ is in the closure of $t$.
Set.MapsTo.closure_left theorem
{t : Set Y} (h : MapsTo f s t) (hc : Continuous f) (ht : IsClosed t) : MapsTo f (closure s) t
Full source 
/-- If a continuous map `f` maps `s` to a closed set `t`, then it maps `closure s` to `t`. -/
theorem Set.MapsTo.closure_left {t : Set Y} (h : MapsTo f s t)
    (hc : Continuous f) (ht : IsClosed t) : MapsTo f (closure s) t :=
  ht.closure_eq ▸ h.closure hc
Continuous Functions Preserve Closure Mapping to Closed Sets
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a continuous function, and $s \subseteq X$, $t \subseteq Y$ subsets such that $f$ maps $s$ into $t$. If $t$ is closed in $Y$, then $f$ maps the closure of $s$ into $t$.
Filter.Tendsto.lift'_closure theorem
(hf : Continuous f) {l l'} (h : Tendsto f l l') : Tendsto f (l.lift' closure) (l'.lift' closure)
Full source 
theorem Filter.Tendsto.lift'_closure (hf : Continuous f) {l l'} (h : Tendsto f l l') :
    Tendsto f (l.lift' closure) (l'.lift' closure) :=
  tendsto_lift'.2 fun s hs ↦ by
    filter_upwards [mem_lift' (h hs)] using (mapsTo_preimage _ _).closure hf
Continuous Functions Preserve Filter Limits Under Closure Lifting
Informal description
Let $X$ and $Y$ be topological spaces and $f \colon X \to Y$ be a continuous function. If $f$ tends to filter $l'$ along filter $l$, then $f$ also tends to the closure-lifted filter of $l'$ along the closure-lifted filter of $l$.
tendsto_lift'_closure_nhds theorem
(hf : Continuous f) (x : X) : Tendsto f ((𝓝 x).lift' closure) ((𝓝 (f x)).lift' closure)
Full source 
theorem tendsto_lift'_closure_nhds (hf : Continuous f) (x : X) :
    Tendsto f ((𝓝 x).lift' closure) ((𝓝 (f x)).lift' closure) :=
  (hf.tendsto x).lift'_closure hf
Continuous Functions Preserve Closure-Lifted Neighborhood Filters
Informal description
Let $X$ and $Y$ be topological spaces and $f \colon X \to Y$ be a continuous function. For any point $x \in X$, the function $f$ maps the closure-lifted neighborhood filter of $x$ to the closure-lifted neighborhood filter of $f(x)$. In other words, $f$ preserves limits under closure lifting at every point.
Function.Surjective.denseRange theorem
(hf : Function.Surjective f) : DenseRange f
Full source 
/-- A surjective map has dense range. -/
theorem Function.Surjective.denseRange (hf : Function.Surjective f) : DenseRange f := fun x => by
  simp [hf.range_eq]
Surjective Functions Have Dense Range
Informal description
If a function $f \colon X \to Y$ between topological spaces is surjective, then its range is dense in $Y$.
denseRange_iff_closure_range theorem
: DenseRange f ↔ closure (range f) = univ
Full source 
theorem denseRange_iff_closure_range : DenseRangeDenseRange f ↔ closure (range f) = univ :=
  dense_iff_closure_eq
Characterization of Dense Range via Closure: $\overline{\mathrm{range}(f)} = Y$
Informal description
A function $f \colon X \to Y$ between topological spaces has dense range if and only if the closure of its range is equal to the entire codomain $Y$, i.e., $\overline{\mathrm{range}(f)} = Y$.
DenseRange.closure_range theorem
(h : DenseRange f) : closure (range f) = univ
Full source 
theorem DenseRange.closure_range (h : DenseRange f) : closure (range f) = univ :=
  h.closure_eq
Closure of Range Equals Universe for Dense Range Functions
Informal description
For a function $f : X \to Y$ between topological spaces, if $f$ has dense range (i.e., the image of $f$ is dense in $Y$), then the closure of the range of $f$ is equal to the entire space $Y$.
denseRange_subtype_val theorem
{p : X → Prop} : DenseRange (@Subtype.val _ p) ↔ Dense {x | p x}
Full source 
@[simp]
lemma denseRange_subtype_val {p : X → Prop} : DenseRangeDenseRange (@Subtype.val _ p) ↔ Dense {x | p x} := by
  simp [DenseRange]
Density of Subtype Inclusion vs. Density of Predicate Set
Informal description
For a topological space $X$ and a predicate $p : X \to \text{Prop}$, the range of the inclusion map $\text{Subtype.val} : \{x \mid p x\} \to X$ is dense in $X$ if and only if the set $\{x \mid p x\}$ is dense in $X$.
Dense.denseRange_val theorem
(h : Dense s) : DenseRange ((↑) : s → X)
Full source 
theorem Dense.denseRange_val (h : Dense s) : DenseRange ((↑) : s → X) :=
  denseRange_subtype_val.2 h
Density of Subset Implies Density of Inclusion Map
Informal description
For a dense subset $s$ of a topological space $X$, the inclusion map $(\uparrow) : s \to X$ has dense range in $X$.
Continuous.range_subset_closure_image_dense theorem
{f : X → Y} (hf : Continuous f) (hs : Dense s) : range f ⊆ closure (f '' s)
Full source 
theorem Continuous.range_subset_closure_image_dense {f : X → Y} (hf : Continuous f)
    (hs : Dense s) : rangerange f ⊆ closure (f '' s) := by
  rw [← image_univ, ← hs.closure_eq]
  exact image_closure_subset_closure_image hf
Range of Continuous Function Contained in Closure of Image of Dense Set
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a continuous function, and $s \subseteq X$ a dense subset. Then the range of $f$ is contained in the closure of the image of $s$ under $f$, i.e., $$\text{range}(f) \subseteq \overline{f(s)}.$$
DenseRange.dense_image theorem
{f : X → Y} (hf' : DenseRange f) (hf : Continuous f) (hs : Dense s) : Dense (f '' s)
Full source 
/-- The image of a dense set under a continuous map with dense range is a dense set. -/
theorem DenseRange.dense_image {f : X → Y} (hf' : DenseRange f) (hf : Continuous f)
    (hs : Dense s) : Dense (f '' s) :=
  (hf'.mono <| hf.range_subset_closure_image_dense hs).of_closure
Density Preservation under Continuous Maps with Dense Range
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a continuous function with dense range, and $s \subseteq X$ a dense subset. Then the image $f(s)$ is dense in $Y$.
DenseRange.subset_closure_image_preimage_of_isOpen theorem
(hf : DenseRange f) (hs : IsOpen s) : s ⊆ closure (f '' (f ⁻¹' s))
Full source 
/-- 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.subset_closure_image_preimage_of_isOpen (hf : DenseRange f) (hs : IsOpen s) :
    s ⊆ closure (f '' (f ⁻¹' s)) := by
  rw [image_preimage_eq_inter_range]
  exact hf.open_subset_closure_inter hs
Open Sets are Dense in Their Preimage Image for Functions with Dense Range
Informal description
Let $f : X \to Y$ be a function with dense range, and let $s \subseteq Y$ be an open set. Then $s$ is contained in the closure of the image of its preimage under $f$, i.e., $s \subseteq \overline{f(f^{-1}(s))}$.
DenseRange.dense_of_mapsTo theorem
{f : X → Y} (hf' : DenseRange f) (hf : Continuous f) (hs : Dense s) {t : Set Y} (ht : MapsTo f s t) : Dense t
Full source 
/-- If a continuous map with dense range maps a dense set to a subset of `t`, then `t` is a dense
set. -/
theorem DenseRange.dense_of_mapsTo {f : X → Y} (hf' : DenseRange f) (hf : Continuous f)
    (hs : Dense s) {t : Set Y} (ht : MapsTo f s t) : Dense t :=
  (hf'.dense_image hf hs).mono ht.image_subset
Density Transfer via Continuous Maps with Dense Range
Informal description
Let $X$ and $Y$ be topological spaces, $f \colon X \to Y$ a continuous function with dense range, and $s \subseteq X$ a dense subset. If $f$ maps $s$ into a subset $t \subseteq Y$, then $t$ is dense in $Y$.
DenseRange.comp theorem
{g : Y → Z} {f : α → Y} (hg : DenseRange g) (hf : DenseRange f) (cg : Continuous g) : DenseRange (g ∘ f)
Full source 
/-- Composition of a continuous map with dense range and a function with dense range has dense
range. -/
theorem DenseRange.comp {g : Y → Z} {f : α → Y} (hg : DenseRange g) (hf : DenseRange f)
    (cg : Continuous g) : DenseRange (g ∘ f) := by
  rw [DenseRange, range_comp]
  exact hg.dense_image cg hf
Density Preservation under Composition of Continuous Maps with Dense Range
Informal description
Let $X$, $Y$, and $Z$ be topological spaces, and let $f \colon \alpha \to Y$ and $g \colon Y \to Z$ be functions. If $f$ has dense range, $g$ has dense range and is continuous, then the composition $g \circ f$ has dense range in $Z$.
DenseRange.nonempty theorem
[h : Nonempty X] (hf : DenseRange f) : Nonempty α
Full source 
theorem DenseRange.nonempty [h : Nonempty X] (hf : DenseRange f) : Nonempty α :=
  hf.nonempty_iff.mpr h
Nonempty domain for function with dense range and nonempty codomain
Informal description
If $X$ is a nonempty topological space and $f \colon \alpha \to X$ has dense range, then the domain $\alpha$ is nonempty.
DenseRange.some definition
(hf : DenseRange f) (x : X) : α
Full source 
/-- Given a function `f : X → Y` with dense range and `y : Y`, returns some `x : X`. -/
noncomputable def DenseRange.some (hf : DenseRange f) (x : X) : α :=
  Classical.choice <| hf.nonempty_iff.mpr ⟨x⟩
Choice of preimage for a function with dense range
Informal description
Given a function \( f : X \to Y \) with dense range and an element \( x \in X \), returns some element in the domain \( X \). The choice is made using the axiom of choice, ensuring the existence of such an element due to the density of the range of \( f \).
DenseRange.exists_mem_open theorem
(hf : DenseRange f) (ho : IsOpen s) (hs : s.Nonempty) : ∃ a, f a ∈ s
Full source 
nonrec theorem DenseRange.exists_mem_open (hf : DenseRange f) (ho : IsOpen s) (hs : s.Nonempty) :
    ∃ a, f a ∈ s :=
  exists_range_iff.1 <| hf.exists_mem_open ho hs
Existence of Preimage in Open Set for Dense Range Function
Informal description
Let $f : X \to Y$ be a function between topological spaces with dense range, and let $s \subseteq Y$ be a nonempty open set. Then there exists an element $a \in X$ such that $f(a) \in s$.
DenseRange.mem_nhds theorem
(h : DenseRange f) (hs : s ∈ 𝓝 x) : ∃ a, f a ∈ s
Full source 
theorem DenseRange.mem_nhds (h : DenseRange f) (hs : s ∈ 𝓝 x) :
    ∃ a, f a ∈ s :=
  let ⟨a, ha⟩ := h.exists_mem_open isOpen_interior ⟨x, mem_interior_iff_mem_nhds.2 hs⟩
  ⟨a, interior_subset ha⟩
Dense range functions intersect every neighborhood
Informal description
Let $f : X \to Y$ be a function between topological spaces with dense range, and let $s$ be a neighborhood of $x$ in $Y$. Then there exists an element $a \in X$ such that $f(a) \in s$.