def pairing {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (f : X → Y) (g : X → Z) : X → Y × Z

Definition 2.2: Pairing of functions. For functions f : X → Y and g : X → Z, the pairing (f,g) is the function X → Y × Z given by x ↦ (f x, g x).

Equations

• pairing f g x = (f x, g x)

theorem continuousAt_and_continuous_pairing_iff {X : Type u_1} [TopologicalSpace X] (f g : X → ℝ) : (∀ (x0 : X), ContinuousAt f x0 ∧ ContinuousAt g x0 ↔ ContinuousAt (pairing f g) x0) ∧ (Continuous f ∧ Continuous g ↔ Continuous (pairing f g))

Lemma 2.1: For functions f, g : X → ℝ and their direct sum (f, g) : X → ℝ × ℝ with the Euclidean metric: (a) for any x0, f and g are both continuous at x0 iff (f, g) is continuous at x0; (b) f and g are both continuous iff (f, g) is continuous.

theorem continuous_real_operations_and_scalar_mul : (Continuous fun (p : ℝ × ℝ) => p.1 + p.2) ∧ (Continuous fun (p : ℝ × ℝ) => p.1 - p.2) ∧ (Continuous fun (p : ℝ × ℝ) => p.1 * p.2) ∧ (Continuous fun (p : ℝ × ℝ) => max p.1 p.2) ∧ (Continuous fun (p : ℝ × ℝ) => min p.1 p.2) ∧ (Continuous fun (p : ℝ × { y : ℝ // y ≠ 0 }) => p.1 / ↑p.2) ∧ ∀ (c : ℝ), Continuous fun (x : ℝ) => c * x

Lemma 2.2: The functions +, -, ·, max, and min on ℝ × ℝ are continuous; the division function (x,y) ↦ x / y is continuous on ℝ × (ℝ \ {0}); and for each c : ℝ, the function m_c(x) = c * x is continuous.

theorem helperForTheorem_2_4_continuousAt_const_mul {X : Type u_1} [TopologicalSpace X] (c : ℝ) {f : X → ℝ} {x0 : X} (hf : ContinuousAt f x0) : ContinuousAt (fun (x : X) => c * f x) x0

Helper for Theorem 2.4: continuity of constant multiplication at a point.

theorem helperForTheorem_2_4_continuous_const_mul {X : Type u_1} [TopologicalSpace X] (c : ℝ) {f : X → ℝ} (hf : Continuous f) : Continuous fun (x : X) => c * f x

Helper for Theorem 2.4: continuity of constant multiplication.

theorem helperForTheorem_2_4_continuousAt_div_of_forall_ne_zero {X : Type u_1} [TopologicalSpace X] {f g : X → ℝ} {x0 : X} (hf : ContinuousAt f x0) (hg : ContinuousAt g x0) (hgnz : ∀ (x : X), g x ≠ 0) : ContinuousAt (fun (x : X) => f x / g x) x0

Helper for Theorem 2.4: continuity of division under a global nonvanishing.

theorem continuous_operations_at_and_continuous {X : Type u_1} [MetricSpace X] (f g : X → ℝ) (c : ℝ) (x0 : X) : (ContinuousAt f x0 ∧ ContinuousAt g x0 → ContinuousAt (fun (x : X) => f x + g x) x0 ∧ ContinuousAt (fun (x : X) => f x - g x) x0 ∧ ContinuousAt (fun (x : X) => f x * g x) x0 ∧ ContinuousAt (fun (x : X) => max (f x) (g x)) x0 ∧ ContinuousAt (fun (x : X) => min (f x) (g x)) x0 ∧ ContinuousAt (fun (x : X) => c * f x) x0 ∧ ((∀ (x : X), g x ≠ 0) → ContinuousAt (fun (x : X) => f x / g x) x0)) ∧ (Continuous f ∧ Continuous g → (Continuous fun (x : X) => f x + g x) ∧ (Continuous fun (x : X) => f x - g x) ∧ (Continuous fun (x : X) => f x * g x) ∧ (Continuous fun (x : X) => max (f x) (g x)) ∧ (Continuous fun (x : X) => min (f x) (g x)) ∧ (Continuous fun (x : X) => c * f x) ∧ ((∀ (x : X), g x ≠ 0) → Continuous fun (x : X) => f x / g x))

Theorem 2.4: (a) If f and g are continuous at x0, then f + g, f - g, f g, max f g, min f g, and c f are continuous at x0, and if g(x) ≠ 0 for all x, then f/g is continuous at x0. (b) If f and g are continuous, then the same operations are continuous, and if g(x) ≠ 0 for all x, then f/g is continuous.

theorem continuous_abs_comp {X : Type u_1} [MetricSpace X] (f : X → ℝ) (hf : Continuous f) : Continuous fun (x : X) => |f x|

Proposition 2.6: If f : X → ℝ is continuous on a metric space, then the function |f| defined by |f| (x) = |f x| is continuous on X.

theorem continuous_projections_and_coordinate_comp : ((Continuous fun (p : ℝ × ℝ) => p.1) ∧ Continuous fun (p : ℝ × ℝ) => p.2) ∧ ∀ {X : Type u_1} [inst : MetricSpace X] {f : ℝ → X}, Continuous f → (Continuous fun (p : ℝ × ℝ) => f p.1) ∧ Continuous fun (p : ℝ × ℝ) => f p.2

Proposition 2.7: The coordinate projections π₁, π₂ : ℝ × ℝ → ℝ are continuous, and if (X, d) is a metric space with f : ℝ → X continuous, then g₁(x,y) = f x and g₂(x,y) = f y are continuous.

theorem helperForProposition_2_8_continuous_monomial (c0 : ℝ) (i j : ℕ) : Continuous fun (p : ℝ × ℝ) => c0 * p.1 ^ i * p.2 ^ j

Helper for Proposition 2.8: continuity of a single monomial term.

theorem helperForProposition_2_8_continuous_double_sum (n m : ℕ) (c : ℕ → ℕ → ℝ) : Continuous fun (p : ℝ × ℝ) => ∑ i ∈ Finset.range (n + 1), ∑ j ∈ Finset.range (m + 1), c i j * p.1 ^ i * p.2 ^ j

Helper for Proposition 2.8: continuity of the finite double sum defining P.

theorem helperForProposition_2_8_continuous_comp {X : Type u_1} [MetricSpace X] {P : ℝ × ℝ → ℝ} (hP : Continuous P) {f g : X → ℝ} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : X) => P (f x, g x)

Helper for Proposition 2.8: continuity after composing with a pair of continuous maps.

theorem continuous_polynomial_two_variables (n m : ℕ) (c : ℕ → ℕ → ℝ) : have P := fun (p : ℝ × ℝ) => ∑ i ∈ Finset.range (n + 1), ∑ j ∈ Finset.range (m + 1), c i j * p.1 ^ i * p.2 ^ j; Continuous P ∧ ∀ {X : Type u_1} [inst : MetricSpace X] {f g : X → ℝ}, Continuous f → Continuous g → Continuous fun (x : X) => P (f x, g x)

Proposition 2.8: For integers n, m ≥ 0 and coefficients c_{ij} ∈ ℝ, define P(x,y) = ∑_{i=0}^n ∑_{j=0}^m c_{ij} x^i y^j. Then P is continuous on ℝ × ℝ. Moreover, for any metric space X and continuous f, g : X → ℝ, the map x ↦ P (f x, g x) is continuous.

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

Helper for Proposition 2.9: continuity of the pairing map into a product.

theorem continuous_pairing_euclidean {X : Type u_1} [TopologicalSpace X] {m n : ℕ} (f : X → EuclideanSpace ℝ (Fin m)) (g : X → EuclideanSpace ℝ (Fin n)) (hf : Continuous f) (hg : Continuous g) : Continuous (pairing f g)

Proposition 2.9: If X is a topological space and f : X → ℝ^m, g : X → ℝ^n are continuous (with the Euclidean topologies), then the map x ↦ (f x, g x) into ℝ^m × ℝ^n ≃ ℝ^{m+n} is continuous.

theorem helperForProposition_2_10_continuous_monomial (k : ℕ) (multi : Fin k → ℕ) : Continuous fun (x : EuclideanSpace ℝ (Fin k)) => ∏ j : Fin k, x.ofLp j ^ multi j

Helper for Proposition 2.10: continuity of a monomial on ℝ^k.

theorem helperForProposition_2_10_continuous_weighted_monomial (k : ℕ) (I : Finset (Fin k → ℕ)) (c : { i : Fin k → ℕ // i ∈ I } → ℝ) (i : { i : Fin k → ℕ // i ∈ I }) : Continuous fun (x : EuclideanSpace ℝ (Fin k)) => c i * ∏ j : Fin k, x.ofLp j ^ ↑i j

Helper for Proposition 2.10: continuity of a weighted monomial term.

theorem continuous_polynomial_multi_index (k : ℕ) (hk : 1 ≤ k) (I : Finset (Fin k → ℕ)) (c : { i : Fin k → ℕ // i ∈ I } → ℝ) : have P := fun (x : EuclideanSpace ℝ (Fin k)) => ∑ i ∈ I.attach, c i * ∏ j : Fin k, x.ofLp j ^ ↑i j; Continuous P

Proposition 2.10: Let k ≥ 1, let I ⊆ ℕ^k be finite, let c : I → ℝ, and define P : ℝ^k → ℝ by P(x_1, ..., x_k) = ∑_{(i_1, ..., i_k) ∈ I} c(i_1, ..., i_k) * x_1^{i_1} * ... * x_k^{i_k}. Then P is continuous on ℝ^k (with the Euclidean topology).

def prodSumDist (X : Type u_1) (Y : Type u_2) [MetricSpace X] [MetricSpace Y] : X × Y → X × Y → ℝ

Sum distance on a product of metric spaces: d((x,y),(x',y')) = dist x x' + dist y y'.

Equations

• prodSumDist X Y p q = dist p.1 q.1 + dist p.2 q.2

theorem helperForProposition_2_11_prodSumDist_self (X : Type u_1) (Y : Type u_2) [MetricSpace X] [MetricSpace Y] (p : X × Y) : prodSumDist X Y p p = 0

Helper for Proposition 2.11: sum distance vanishes on identical points.

theorem helperForProposition_2_11_prodSumDist_comm (X : Type u_1) (Y : Type u_2) [MetricSpace X] [MetricSpace Y] (p q : X × Y) : prodSumDist X Y p q = prodSumDist X Y q p

Helper for Proposition 2.11: sum distance is symmetric.

theorem helperForProposition_2_11_prodSumDist_triangle (X : Type u_1) (Y : Type u_2) [MetricSpace X] [MetricSpace Y] (p q r : X × Y) : prodSumDist X Y p r ≤ prodSumDist X Y p q + prodSumDist X Y q r

Helper for Proposition 2.11: sum distance satisfies the triangle inequality.

theorem helperForProposition_2_11_eq_of_prodSumDist_eq_zero (X : Type u_1) (Y : Type u_2) [MetricSpace X] [MetricSpace Y] {p q : X × Y} : prodSumDist X Y p q = 0 → p = q

Helper for Proposition 2.11: zero sum distance implies equality.

theorem metricSpace_prod_sum_dist (X : Type u_1) (Y : Type u_2) [MetricSpace X] [MetricSpace Y] : ∃ (m : MetricSpace (X × Y)), dist = prodSumDist X Y

Proposition 2.11: For metric spaces (X, d_X) and (Y, d_Y), the function d_{X×Y}((x,y),(x',y')) = d_X(x,x') + d_Y(y,y') is a metric on X × Y, hence (X × Y, d_{X×Y}) is a metric space.

theorem helperForProposition_2_12_eventually_Ioo_of_continuousAt (f : ℝ × ℝ → ℝ) (x0 y0 : ℝ) (hf : ContinuousAt f (x0, y0)) {ε : ℝ} : 0 < ε → ∀ᶠ (x : ℝ) in nhds x0, ∀ᶠ (y : ℝ) in nhds y0, f (x, y) ∈ Set.Ioo (f (x0, y0) - ε) (f (x0, y0) + ε)

Helper for Proposition 2.12: extract a two-variable ε-band from continuity.

theorem helperForProposition_2_12_tendsto_outer_limsup_inner_nhds (f : ℝ × ℝ → ℝ) (x0 y0 : ℝ) (hf : ContinuousAt f (x0, y0)) : Filter.Tendsto (fun (x : ℝ) => Filter.limsup (fun (y : ℝ) => f (x, y)) (nhds y0)) (nhds x0) (nhds (f (x0, y0)))

Helper for Proposition 2.12: outer limsup (inner y) tends to f (x0,y0).

theorem helperForProposition_2_12_tendsto_outer_liminf_inner_nhds (f : ℝ × ℝ → ℝ) (x0 y0 : ℝ) (hf : ContinuousAt f (x0, y0)) : Filter.Tendsto (fun (x : ℝ) => Filter.liminf (fun (y : ℝ) => f (x, y)) (nhds y0)) (nhds x0) (nhds (f (x0, y0)))

Helper for Proposition 2.12: outer liminf (inner y) tends to f (x0,y0).

theorem helperForProposition_2_12_tendsto_nhds_forces_value_at_point {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {x0 : X} {g : X → Y} {a : Y} (h : Filter.Tendsto g (nhds x0) (nhds a)) : g x0 = a

Helper for Proposition 2.12: a nhds-limit forces the point value in a T1 space.

theorem helperForProposition_2_12_limUnder_section_at_point_eq (f : ℝ × ℝ → ℝ) (x0 y0 : ℝ) (hf : ContinuousAt f (x0, y0)) : (limUnder (nhds y0) fun (y : ℝ) => f (x0, y)) = f (x0, y0) ∧ (limUnder (nhds x0) fun (x : ℝ) => f (x, y0)) = f (x0, y0)

Helper for Proposition 2.12: identify section limits at the point.

theorem iterated_limsup_liminf_eq_of_continuousAt (f : ℝ × ℝ → ℝ) (x0 y0 : ℝ) (hf : ContinuousAt f (x0, y0)) : (Filter.Tendsto (fun (x : ℝ) => Filter.limsup (fun (y : ℝ) => f (x, y)) (nhds y0)) (nhds x0) (nhds (f (x0, y0))) ∧ Filter.Tendsto (fun (y : ℝ) => Filter.limsup (fun (x : ℝ) => f (x, y)) (nhds x0)) (nhds y0) (nhds (f (x0, y0)))) ∧ (Filter.Tendsto (fun (x : ℝ) => Filter.liminf (fun (y : ℝ) => f (x, y)) (nhds y0)) (nhds x0) (nhds (f (x0, y0))) ∧ Filter.Tendsto (fun (y : ℝ) => Filter.liminf (fun (x : ℝ) => f (x, y)) (nhds x0)) (nhds y0) (nhds (f (x0, y0)))) ∧ ∀ {L1 L2 : ℝ}, Filter.Tendsto (fun (x : ℝ) => limUnder (nhds y0) fun (y : ℝ) => f (x, y)) (nhds x0) (nhds L1) → Filter.Tendsto (fun (y : ℝ) => limUnder (nhds x0) fun (x : ℝ) => f (x, y)) (nhds y0) (nhds L2) → L1 = L2

Proposition 2.12: If f : ℝ × ℝ → ℝ is continuous at (x0, y0), then lim_{x→x0} limsup_{y→y0} f(x, y) = lim_{y→y0} limsup_{x→x0} f(x, y) = f(x0, y0) and lim_{x→x0} liminf_{y→y0} f(x, y) = lim_{y→y0} liminf_{x→x0} f(x, y) = f(x0, y0). In particular, if both iterated limits exist, then lim_{x→x0} lim_{y→y0} f(x, y) = lim_{y→y0} lim_{x→x0} f(x, y).

theorem continuous_in_each_variable_of_continuous (f : ℝ × ℝ → ℝ) (hf : Continuous f) : (∀ (x : ℝ), Continuous fun (y : ℝ) => f (x, y)) ∧ ∀ (y : ℝ), Continuous fun (x : ℝ) => f (x, y)

Proposition 2.13: A jointly continuous function f : ℝ × ℝ → ℝ is continuous in each variable separately; for each x, the map y ↦ f (x, y) is continuous, and for each y, the map x ↦ f (x, y) is continuous.

noncomputable def separateContinuityExample : ℝ × ℝ → ℝ

The function f(x,y) = xy / (x^2 + y^2) for (x,y) ≠ (0,0), and 0 at (0,0).

Equations

• separateContinuityExample p = if p = (0, 0) then 0 else p.1 * p.2 / (p.1 ^ 2 + p.2 ^ 2)

theorem helperForProposition_2_14_denominator_ne_zero_of_left_ne_zero {x : ℝ} (hx : x ≠ 0) (y : ℝ) : x ^ 2 + y ^ 2 ≠ 0

Helper for Proposition 2.14: nonvanishing of x^2 + y^2 when x ≠ 0.

theorem helperForProposition_2_14_denominator_ne_zero_of_right_ne_zero {y : ℝ} (hy : y ≠ 0) (x : ℝ) : x ^ 2 + y ^ 2 ≠ 0

Helper for Proposition 2.14: nonvanishing of x^2 + y^2 when y ≠ 0.

theorem helperForProposition_2_14_continuous_rational_fix_left {x : ℝ} (hx : x ≠ 0) : Continuous fun (y : ℝ) => x * y / (x ^ 2 + y ^ 2)

Helper for Proposition 2.14: continuity of the rational expression with fixed nonzero x.

theorem helperForProposition_2_14_continuous_rational_fix_right {y : ℝ} (hy : y ≠ 0) : Continuous fun (x : ℝ) => x * y / (x ^ 2 + y ^ 2)

Helper for Proposition 2.14: continuity of the rational expression with fixed nonzero y.

theorem helperForProposition_2_14_simp_section_of_left_ne_zero {x : ℝ} (hx : x ≠ 0) : (fun (y : ℝ) => separateContinuityExample (x, y)) = fun (y : ℝ) => x * y / (x ^ 2 + y ^ 2)

Helper for Proposition 2.14: simplify the y-section when x ≠ 0.

theorem helperForProposition_2_14_simp_section_of_right_ne_zero {y : ℝ} (hy : y ≠ 0) : (fun (x : ℝ) => separateContinuityExample (x, y)) = fun (x : ℝ) => x * y / (x ^ 2 + y ^ 2)

Helper for Proposition 2.14: simplify the x-section when y ≠ 0.

theorem helperForProposition_2_14_section_left_zero : (fun (y : ℝ) => separateContinuityExample (0, y)) = fun (x : ℝ) => 0

Helper for Proposition 2.14: the y-section at x = 0 is identically zero.

theorem helperForProposition_2_14_section_right_zero : (fun (x : ℝ) => separateContinuityExample (x, 0)) = fun (x : ℝ) => 0

Helper for Proposition 2.14: the x-section at y = 0 is identically zero.

theorem continuous_in_each_variable_separateContinuityExample : (∀ (x : ℝ), Continuous fun (y : ℝ) => separateContinuityExample (x, y)) ∧ ∀ (y : ℝ), Continuous fun (x : ℝ) => separateContinuityExample (x, y)

Proposition 2.14: For the function f : ℝ × ℝ → ℝ defined by f(x,y) = xy / (x^2 + y^2) for (x,y) ≠ (0,0) and f(0,0) = 0, (i) for each fixed x, the map y ↦ f(x,y) is continuous on ℝ; (ii) for each fixed y, the map x ↦ f(x,y) is continuous on ℝ.