@[reducible, inline]

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

Definition 2.1 (Continuous functions): (i) For x0 ∈ X, f is continuous at x0 if for every ε > 0 there exists δ > 0 such that for all x ∈ X, d_X x x0 < δ implies d_Y (f x) (f x0) < ε. (ii) f is continuous on X if it is continuous at every x ∈ X.

Equations

• IsContinuousAt f x0 = ContinuousAt f x0

@[reducible, inline]

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

A function between metric spaces is continuous if it is continuous at every point.

Equations

• IsContinuous f = ∀ (x : X), IsContinuousAt f x

theorem continuous_sq_of_continuous {X : Type u_1} [TopologicalSpace X] (f : X → ℝ) : Continuous f → Continuous fun (x : X) => f x ^ 2

Proposition 2.1: Let X be a topological space and let f : X → ℝ be continuous. Define f^2 : X → ℝ by f^2 x := (f x)^2. Then f^2 is continuous.

theorem helperForTheorem_2_1_openImage_iff_continuousAt {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X → Y) (x0 : X) : IsContinuousAt f x0 ↔ ∀ (V : Set Y), IsOpen V → f x0 ∈ V → ∃ (U : Set X), IsOpen U ∧ x0 ∈ U ∧ f '' U ⊆ V

Helper for Theorem 2.1: open-set formulation of continuity at a point.

theorem continuity_preserves_convergence {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X → Y) (x0 : X) : (IsContinuousAt f x0 ↔ ∀ (x : ℕ → X), Filter.Tendsto x Filter.atTop (nhds x0) → Filter.Tendsto (fun (n : ℕ) => f (x n)) Filter.atTop (nhds (f x0))) ∧ (IsContinuousAt f x0 ↔ ∀ (V : Set Y), IsOpen V → f x0 ∈ V → ∃ (U : Set X), IsOpen U ∧ x0 ∈ U ∧ f '' U ⊆ V)

Theorem 2.1 (Continuity preserves convergence): Let (X,d_X) and (Y,d_Y) be metric spaces, f : X → Y, and x0 ∈ X. The following statements are equivalent: (a) f is continuous at x0. (b) For every sequence x : ℕ → X with x → x0, one has f ∘ x → f x0. (c) For every open set V ⊆ Y with f x0 ∈ V, there exists an open set U ⊆ X with x0 ∈ U such that f '' U ⊆ V.

theorem isContinuous_inclusion_subtype {X : Type u_1} [MetricSpace X] (E : Set X) : IsContinuous Subtype.val

Proposition 2.2: Let (X, d) be a metric space and let (E, d|_{E × E}) be a subspace of (X, d). The inclusion map ι_{E → X} : E → X, defined by ι_{E → X}(x) = x, is continuous.

theorem helperForTheorem_2_2_isContinuous_iff_continuous {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X → Y) : IsContinuous f ↔ Continuous f

Helper for Theorem 2.2: IsContinuous matches Continuous for metric spaces.

theorem continuous_iff_sequential_iff_preimage_open_iff_preimage_closed {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X → Y) : (IsContinuous f ↔ ∀ (x0 : X) (x : ℕ → X), Filter.Tendsto x Filter.atTop (nhds x0) → Filter.Tendsto (fun (n : ℕ) => f (x n)) Filter.atTop (nhds (f x0))) ∧ (IsContinuous f ↔ ∀ (V : Set Y), IsOpen V → IsOpen (f ⁻¹' V)) ∧ (IsContinuous f ↔ ∀ (F : Set Y), IsClosed F → IsClosed (f ⁻¹' F))

Theorem 2.2: Let (X, d_X) and (Y, d_Y) be metric spaces and f : X → Y. The following statements are equivalent: (a) f is continuous. (b) Whenever a sequence x in X converges to x0, the sequence fun n => f (x n) converges to f x0. (c) For every open set V ⊆ Y, the preimage f ⁻¹' V is open in X. (d) For every closed set F ⊆ Y, the preimage f ⁻¹' F is closed in X.

theorem helperForProposition_2_3_restrict_isContinuousAt {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X → Y) (E : Set X) (x0 : ↑E) : IsContinuousAt f ↑x0 → IsContinuousAt (fun (x : ↑E) => f ↑x) x0

Helper for Proposition 2.3: continuity at a point is preserved under restriction to a subset.

theorem helperForProposition_2_3_restrict_isContinuous {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X → Y) (E : Set X) : IsContinuous f → IsContinuous fun (x : ↑E) => f ↑x

Helper for Proposition 2.3: global continuity is preserved under restriction to a subset.

theorem continuous_restrict_of_continuous {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X → Y) (E : Set X) : (∀ (x0 : ↑E), IsContinuousAt f ↑x0 → IsContinuousAt (fun (x : ↑E) => f ↑x) x0) ∧ (IsContinuous f → IsContinuous fun (x : ↑E) => f ↑x)

Proposition 2.3: If f : X → Y is continuous at x0 ∈ E, then the restriction f|_E is continuous at x0; in particular, if f is continuous on X, then f|_E is continuous on E.

theorem continuity_preserved_by_composition {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [MetricSpace X] [MetricSpace Y] [MetricSpace Z] : (∀ (f : X → Y) (g : Y → Z) (x0 : X), IsContinuousAt f x0 → IsContinuousAt g (f x0) → IsContinuousAt (fun (x : X) => g (f x)) x0) ∧ ∀ (f : X → Y) (g : Y → Z), IsContinuous f → IsContinuous g → IsContinuous fun (x : X) => g (f x)

Theorem 2.3 (Continuity preserved by composition): Let (X,d_X), (Y,d_Y), and (Z,d_Z) be metric spaces. (a) If f : X → Y is continuous at x0 and g : Y → Z is continuous at f x0, then g ∘ f is continuous at x0. (b) If f is continuous on X and g is continuous on Y, then g ∘ f is continuous on X.

theorem continuousAt_codomainRestrict_iff {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (f : X → Y) (E : Set Y) (hE : ∀ (x : X), f x ∈ E) (x0 : X) : IsContinuousAt f x0 ↔ IsContinuousAt (Set.codRestrict f E hE) x0

Proposition 2.4: Let f : X → Y be a function between metric spaces, and let E ⊆ Y contain the image of f. Let g : X → E be the codomain restriction of f with g x = f x. Then for any x0 ∈ X, f is continuous at x0 iff g is continuous at x0.