def metricContinuousAt {X : Type u} [PseudoMetricSpace X] {Y : Type v} [PseudoMetricSpace Y] (f : X → Y) (c : X) : Prop

Definition 7.5.1. A function f : X → Y between metric spaces is continuous at c if for every ε > 0 there is δ > 0 such that dist x c < δ implies dist (f x) (f c) < ε. When this holds for every c, the function is continuous.

Equations

• metricContinuousAt f c = ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : X⦄, dist x c < δ → dist (f x) (f c) < ε

theorem metricContinuousAt_iff_continuousAt {X : Type u} [PseudoMetricSpace X] {Y : Type v} [PseudoMetricSpace Y] (f : X → Y) (c : X) : metricContinuousAt f c ↔ ContinuousAt f c

The book's ε-δ continuity at a point agrees with mathlib's ContinuousAt.

theorem continuousAt_iff_tendsto_seq {X : Type u} [PseudoMetricSpace X] {Y : Type v} [PseudoMetricSpace Y] {f : X → Y} {c : X} : ContinuousAt f c ↔ ∀ (x : ℕ → X), Filter.Tendsto x Filter.atTop (nhds c) → Filter.Tendsto (fun (n : ℕ) => f (x n)) Filter.atTop (nhds (f c))

Proposition 7.5.2. A map between metric spaces is continuous at c if and only if every sequence converging to c has image sequence converging to f c.

def metricContinuous {X : Type u} [PseudoMetricSpace X] {Y : Type v} [PseudoMetricSpace Y] (f : X → Y) : Prop

A function is (globally) continuous when it is continuous at every point.

Equations

• metricContinuous f = ∀ (c : X), metricContinuousAt f c

theorem metricContinuous_iff_continuous {X : Type u} [PseudoMetricSpace X] {Y : Type v} [PseudoMetricSpace Y] (f : X → Y) : metricContinuous f ↔ Continuous f

The book's notion of a continuous function coincides with Continuous.

theorem polynomial_two_vars_continuous (p : MvPolynomial (Fin 2) ℝ) : Continuous fun (x : Fin 2 → ℝ) => (MvPolynomial.eval x) p

Example 7.5.3. A polynomial on ℝ × ℝ (and more generally on finitely many variables) defines a continuous function.

theorem polynomial_finite_vars_continuous {n : ℕ} (p : MvPolynomial (Fin n) ℝ) : Continuous fun (x : Fin n → ℝ) => (MvPolynomial.eval x) p

theorem continuousAt_complex_iff_real_im {X : Type u} [PseudoMetricSpace X] {f : X → ℂ} {c : X} : ContinuousAt f c ↔ ContinuousAt (fun (x : X) => (f x).re) c ∧ ContinuousAt (fun (x : X) => (f x).im) c

Example 7.5.4. A complex-valued function on a metric space is continuous at c exactly when its real and imaginary parts are continuous at c.

theorem compact_image_of_continuous {X : Type u} [PseudoMetricSpace X] {Y : Type v} [PseudoMetricSpace Y] {f : X → Y} (hf : Continuous f) {K : Set X} (hK : IsCompact K) : IsCompact (f '' K)

Lemma 7.5.5. A continuous function maps compact sets to compact sets.

theorem continuous_on_compact_real_extrema {X : Type u} [PseudoMetricSpace X] [CompactSpace X] [Nonempty X] {f : X → ℝ} (hf : Continuous f) : ∃ (x_min : X) (x_max : X), ∀ (x : X), f x_min ≤ f x ∧ f x ≤ f x_max

Theorem 7.5.6. A continuous real-valued function on a nonempty compact metric space is bounded and attains both its absolute minimum and maximum.

theorem continuousAt_iff_preimage_open_nhds {X : Type u} [PseudoMetricSpace X] {Y : Type v} [PseudoMetricSpace Y] {f : X → Y} {c : X} : ContinuousAt f c ↔ ∀ ⦃U : Set Y⦄, IsOpen U → f c ∈ U → ∃ (V : Set X), IsOpen V ∧ c ∈ V ∧ V ⊆ f ⁻¹' U

Lemma 7.5.7. A function between metric spaces is continuous at a point exactly when every open neighborhood of its value has a preimage that is an open neighborhood of the point.

theorem continuous_iff_preimage_open {X : Type u} [PseudoMetricSpace X] {Y : Type v} [PseudoMetricSpace Y] {f : X → Y} : Continuous f ↔ ∀ (U : Set Y), IsOpen U → IsOpen (f ⁻¹' U)

Theorem 7.5.8. A function between metric spaces is continuous if and only if for every open set in the codomain, its preimage is open in the domain.

theorem preimage_closed_of_continuous {X : Type u} [PseudoMetricSpace X] {Y : Type v} [PseudoMetricSpace Y] {f : X → Y} (hf : Continuous f) {E : Set Y} (hE : IsClosed E) : IsClosed (f ⁻¹' E)

Example 7.5.9. For a continuous function, closed sets pull back to closed sets. In particular, if f : X → ℝ is continuous, then its zero set and its nonnegative set are closed, while the positive set is open.

theorem zero_set_closed_of_continuous {X : Type u} [PseudoMetricSpace X] {f : X → ℝ} (hf : Continuous f) : IsClosed {x : X | f x = 0}

theorem nonneg_preimage_closed_of_continuous {X : Type u} [PseudoMetricSpace X] {f : X → ℝ} (hf : Continuous f) : IsClosed {x : X | 0 ≤ f x}

theorem pos_preimage_open_of_continuous {X : Type u} [PseudoMetricSpace X] {f : X → ℝ} (hf : Continuous f) : IsOpen {x : X | 0 < f x}

def metricUniformContinuous {X : Type u} [PseudoMetricSpace X] {Y : Type v} [PseudoMetricSpace Y] (f : X → Y) : Prop

Definition 7.5.10. A function between metric spaces is uniformly continuous if for every ε > 0 there exists δ > 0 such that dist p q < δ implies dist (f p) (f q) < ε.

Equations

• metricUniformContinuous f = ∀ ε > 0, ∃ δ > 0, ∀ ⦃p q : X⦄, dist p q < δ → dist (f p) (f q) < ε

theorem metricUniformContinuous_iff_uniformContinuous {X : Type u} [PseudoMetricSpace X] {Y : Type v} [PseudoMetricSpace Y] (f : X → Y) : metricUniformContinuous f ↔ UniformContinuous f

The book's notion of uniform continuity agrees with mathlib's UniformContinuous.

theorem continuous_uniformContinuous_of_compact {X : Type u} [PseudoMetricSpace X] {Y : Type v} [PseudoMetricSpace Y] [CompactSpace X] {f : X → Y} (hf : Continuous f) : UniformContinuous f

Theorem 7.5.11. A continuous function from a compact metric space to another metric space is uniformly continuous.

theorem intervalIntegral_continuous_on_rectangle {a b c d : ℝ} (f : ℝ → ℝ → ℝ) (hf : Continuous fun (p : ℝ × ℝ) => f p.1 p.2) : Continuous fun (y : ↑(Set.Icc c d)) => ∫ (x : ℝ) in a..b, f x ↑y

Proposition 7.5.12. If f : [a,b] × [c,d] → ℝ is continuous, then g : [c,d] → ℝ defined by g y = ∫ x in a..b, f (x,y) is continuous.

theorem lipschitz_uniformContinuous {X : Type u} [PseudoMetricSpace X] {Y : Type v} [PseudoMetricSpace Y] {K : NNReal} {f : X → Y} (hf : LipschitzWith K f) : UniformContinuous f

Example 7.5.13. A K-Lipschitz map between metric spaces is uniformly continuous. Conversely, the square root on [0,1] is uniformly continuous but fails to be Lipschitz.

theorem sqrt_uniformContinuous_on_Icc : UniformContinuous fun (x : ↑(Set.Icc 0 1)) => √↑x

theorem sqrt_not_Lipschitz_on_Icc : ¬∃ (K : NNReal), LipschitzWith K fun (x : ↑(Set.Icc 0 1)) => √↑x

def metricClusterPoint {X : Type u} [PseudoMetricSpace X] (p : X) (S : Set X) : Prop

Definition 7.5.14. In a metric space (X, d) and subset S, a point p is a cluster point of S if every open ball around p meets S at some point other than p.

Equations

• metricClusterPoint p S = ∀ ε > 0, (Metric.ball p ε ∩ (S \ {p})).Nonempty

theorem metricClusterPoint_iff_mem_closure_diff {X : Type u} [PseudoMetricSpace X] (p : X) (S : Set X) : metricClusterPoint p S ↔ p ∈ closure (S \ {p})

The book's notion of cluster point agrees with the topological description as belonging to the closure of S \ {p}.

def metricLimitWithin {X : Type u} [PseudoMetricSpace X] {Y : Type v} [PseudoMetricSpace Y] (f : X → Y) (S : Set X) (p : X) (L : Y) : Prop

Definition 7.5.15. For metric spaces (X, d_X), (Y, d_Y), subset S, and cluster point p of S, a function f : X → Y has limit L at p along S when every punctured neighborhood of p in S is sent within any ε-ball around L. If the limit is unique we write lim_{x → p} f x = L.

Equations

• metricLimitWithin f S p L = ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : X⦄, x ∈ S → x ≠ p → dist x p < δ → dist (f x) L < ε

theorem metricLimitWithin_iff_tendsto {X : Type u} [PseudoMetricSpace X] {Y : Type v} [PseudoMetricSpace Y] (f : X → Y) (S : Set X) (p : X) (L : Y) : metricLimitWithin f S p L ↔ Filter.Tendsto f (nhdsWithin p (S \ {p})) (nhds L)

The ε-δ limit within a set agrees with mathlib's Tendsto along the punctured neighborhood filter.

theorem metricLimitWithin_unique {X : Type u} [PseudoMetricSpace X] {Y : Type v} [PseudoMetricSpace Y] {S : Set X} {p : X} {f : X → Y} {L₁ L₂ : Y} [T2Space Y] (hp : metricClusterPoint p S) (h₁ : metricLimitWithin f S p L₁) (h₂ : metricLimitWithin f S p L₂) : L₁ = L₂

Proposition 7.5.16. If p is a cluster point of S and a function has a limit along S at p, that limit is unique.

theorem metricLimitWithin_iff_tendsto_seq {X : Type u} [PseudoMetricSpace X] {Y : Type v} [PseudoMetricSpace Y] {S : Set X} {p : X} {f : X → Y} {L : Y} (hp : metricClusterPoint p S) : metricLimitWithin f S p L ↔ ∀ (x : ℕ → X), (∀ (n : ℕ), x n ∈ S \ {p}) → Filter.Tendsto x Filter.atTop (nhds p) → Filter.Tendsto (fun (n : ℕ) => f (x n)) Filter.atTop (nhds L)

Lemma 7.5.17. A function on a subset of a metric space has limit L at a cluster point p of the subset exactly when every sequence in the subset avoiding p and converging to p has image sequence converging to L.