theorem continuous_maps_preserve_compactness {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) {K : Set X} (hK : IsCompact K) : IsCompact (f '' K)

Theorem 2.5: [Continuous maps preserve compactness] If f : X → Y is continuous between metric spaces and K ⊆ X is compact, then the image f '' K is compact.

theorem helperForProposition_2_15_abs_bound {X : Type u_1} [MetricSpace X] [CompactSpace X] {f : X → ℝ} (hf : Continuous f) : ∃ (M : ℝ), ∀ (x : X), |f x| ≤ M

Helper for Proposition 2.15: a continuous real-valued function on a compact metric space is bounded in absolute value.

theorem helperForProposition_2_15_exists_argmax_argmin {X : Type u_1} [MetricSpace X] [CompactSpace X] {f : X → ℝ} (hf : Continuous f) (hne : Nonempty X) : ∃ (x_max : X) (x_min : X), (∀ (x : X), f x ≤ f x_max) ∧ ∀ (x : X), f x_min ≤ f x

Helper for Proposition 2.15: existence of points attaining the maximum and minimum on a compact metric space.

theorem maximum_principle {X : Type u_1} [MetricSpace X] [CompactSpace X] {f : X → ℝ} (hf : Continuous f) : (∃ (M : ℝ), ∀ (x : X), |f x| ≤ M) ∧ (Nonempty X → ∃ (x_max : X) (x_min : X), (∀ (x : X), f x ≤ f x_max) ∧ ∀ (x : X), f x_min ≤ f x)

Proposition 2.15: [Maximum principle] Let (X, d) be a compact metric space and f : X → ℝ continuous. (i) The function f is bounded on X. (ii) If X ≠ ∅, then there exist x_max, x_min : X such that f x_max is a maximum and f x_min is a minimum of f on X.

@[reducible, inline]

abbrev IsUniformlyContinuous {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X → Y) : Prop

Definition 2.6: [Uniform continuity] Let (X, d_X) and (Y, d_Y) be metric spaces and f : X → Y. The function f is uniformly continuous on X if for every ε > 0 there exists δ > 0 such that for all x, x' ∈ X, d_X x x' < δ → d_Y (f x) (f x') < ε.

Equations

• IsUniformlyContinuous f = UniformContinuous f

theorem isUniformlyContinuous_iff_uniformContinuous {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X → Y) : IsUniformlyContinuous f ↔ UniformContinuous f

The predicate IsUniformlyContinuous coincides with mathlib's UniformContinuous.

theorem continuous_iff_uniformlyContinuous_of_compact {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] [CompactSpace X] {f : X → Y} : Continuous f ↔ IsUniformlyContinuous f

Theorem 2.7: Let (X, d_X) and (Y, d_Y) be metric spaces and assume X is compact. For a function f : X → Y, f is continuous on X if and only if f is uniformly continuous on X.

theorem uniformlyContinuous_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [MetricSpace X] [MetricSpace Y] [MetricSpace Z] {f : X → Y} {g : Y → Z} (hf : IsUniformlyContinuous f) (hg : IsUniformlyContinuous g) : IsUniformlyContinuous (g ∘ f)

Proposition 2.16: If f : X → Y and g : Y → Z are uniformly continuous between metric spaces, then g ∘ f : X → Z is uniformly continuous.

theorem helperForProposition_2_17_dist_finTwo_pair_le_add (a b c d : ℝ) : dist !₂[a, b] !₂[c, d] ≤ dist a c + dist b d

Helper for Proposition 2.17: Euclidean distance in ℝ² is bounded by the sum of coordinate distances.

theorem helperForProposition_2_17_dist_pair_le_add_coords {X : Type u_1} [MetricSpace X] {f g : X → ℝ} (x y : X) : dist !₂[f x, g x] !₂[f y, g y] ≤ dist (f x) (f y) + dist (g x) (g y)

Helper for Proposition 2.17: coordinate-wise bound for paired maps.

theorem uniformlyContinuous_pair {X : Type u_1} [MetricSpace X] {f g : X → ℝ} (hf : IsUniformlyContinuous f) (hg : IsUniformlyContinuous g) : IsUniformlyContinuous fun (x : X) => !₂[f x, g x]

Proposition 2.17: Let (X, d_X) be a metric space, and let f, g : X → ℝ be uniformly continuous. Equip ℝ² with the standard metric d((a, b), (c, d)) = √((a - c)^2 + (b - d)^2). Define (f, g) : X → ℝ² by (f, g)(x) = (f x, g x). Then (f, g) is uniformly continuous.

def coordAdd : EuclideanSpace ℝ (Fin 2) → ℝ

The map a(x,y)=x+y on ℝ², viewed as EuclideanSpace ℝ (Fin 2).

Equations

• coordAdd p = p.ofLp 0 + p.ofLp 1

def coordSub : EuclideanSpace ℝ (Fin 2) → ℝ

The map s(x,y)=x-y on ℝ², viewed as EuclideanSpace ℝ (Fin 2).

Equations

• coordSub p = p.ofLp 0 - p.ofLp 1

def coordMul : EuclideanSpace ℝ (Fin 2) → ℝ

The map m(x,y)=x*y on ℝ², viewed as EuclideanSpace ℝ (Fin 2).

Equations

• coordMul p = p.ofLp 0 * p.ofLp 1

theorem helperForProposition_2_18_dist_coord0_coord1_le_dist (p q : EuclideanSpace ℝ (Fin 2)) : dist (p.ofLp 0) (q.ofLp 0) ≤ dist p q ∧ dist (p.ofLp 1) (q.ofLp 1) ≤ dist p q

Helper for Proposition 2.18: each coordinate distance is bounded by the Euclidean distance.

theorem helperForProposition_2_18_uniformlyContinuous_coordAdd : IsUniformlyContinuous coordAdd

Helper for Proposition 2.18: uniform continuity of coordAdd.

theorem helperForProposition_2_18_uniformlyContinuous_coordSub : IsUniformlyContinuous coordSub

Helper for Proposition 2.18: uniform continuity of coordSub.

theorem helperForProposition_2_18_not_uniformlyContinuous_coordMul : ¬IsUniformlyContinuous coordMul

Helper for Proposition 2.18: coordMul fails uniform continuity on ℝ².

theorem uniformlyContinuous_add_sub_not_mul : IsUniformlyContinuous coordAdd ∧ IsUniformlyContinuous coordSub ∧ ¬IsUniformlyContinuous coordMul

Proposition 2.18: On ℝ² with the Euclidean metric and ℝ with the usual metric, the maps a(x,y)=x+y and s(x,y)=x-y are uniformly continuous, whereas m(x,y)=x*y is not uniformly continuous.

theorem uniformlyContinuous_add_sub {X : Type u_1} [MetricSpace X] {f g : X → ℝ} (hf : IsUniformlyContinuous f) (hg : IsUniformlyContinuous g) : IsUniformlyContinuous (f + g) ∧ IsUniformlyContinuous (f - g)

Proposition 2.19: Let (X, d) be a metric space and let f, g : X → ℝ be uniformly continuous. Then the functions f + g and f - g are uniformly continuous on X.