def MetricCauchySequence (X : Type u) [PseudoMetricSpace X] (x : ℕ → X) : Prop

Definition 7.4.1. A sequence {xₙ} in a metric space is Cauchy when for every ε > 0 there exists M ∈ ℕ such that dist (xₙ) (xₖ) < ε for all n, k ≥ M.

Equations

• MetricCauchySequence X x = ∀ ε > 0, ∃ (M : ℕ), ∀ ⦃n k : ℕ⦄, M ≤ n → M ≤ k → dist (x n) (x k) < ε

theorem metricCauchySequence_iff_cauchySeq {X : Type u} [PseudoMetricSpace X] (x : ℕ → X) : MetricCauchySequence X x ↔ CauchySeq x

The book's notion of a Cauchy sequence agrees with the standard filter based definition in mathlib.

theorem metricCauchySequence_of_tendsto {X : Type u} [PseudoMetricSpace X] {x : ℕ → X} {l : X} (hx : Filter.Tendsto x Filter.atTop (nhds l)) : MetricCauchySequence X x

Proposition 7.4.2. A sequence in a metric space that converges to a point is Cauchy.

def metricCauchyCompleteSpace (X : Type u) [PseudoMetricSpace X] : Prop

Definition 7.4.3. A metric space is complete (Cauchy-complete) when every Cauchy sequence converges to a point of the space.

Equations

• metricCauchyCompleteSpace X = ∀ (x : ℕ → X), MetricCauchySequence X x → ∃ (l : X), Filter.Tendsto x Filter.atTop (nhds l)

theorem metricCauchyCompleteSpace_iff_completeSpace (X : Type u) [PseudoMetricSpace X] : metricCauchyCompleteSpace X ↔ CompleteSpace X

The book's sequential notion of completeness is equivalent to the standard CompleteSpace typeclass in mathlib.

theorem metricCauchyCompleteSpace_euclideanSpace (n : ℕ) : metricCauchyCompleteSpace (EuclideanSpace ℝ (Fin n))

Proposition 7.4.4 (sequential version). Every Cauchy sequence in ℝ^n converges.

instance instCompleteSpace_realEuclideanSpace (n : ℕ) : CompleteSpace (EuclideanSpace ℝ (Fin n))

Proposition 7.4.4. The Euclidean space ℝ^n with its standard metric is complete.

instance instCompleteSpace_continuousMap_interval (a b : ℝ) : CompleteSpace C(↑(Set.Icc a b), ℝ)

Proposition 7.4.5. The metric space of continuous real-valued functions on the closed interval [a,b], equipped with the uniform norm metric, is complete.

instance instCompleteSpace_closed_subset {X : Type u} [PseudoMetricSpace X] [CompleteSpace X] {E : Set X} (hE : IsClosed E) : CompleteSpace ↑E

Proposition 7.4.6. If (X,d) is a complete metric space and E ⊆ X is closed, then E is complete with the subspace metric.

def compactCoverProperty (X : Type u) [PseudoMetricSpace X] (K : Set X) : Prop

Definition 7.4.7. A subset K of a metric space is compact when every open cover of K admits a finite subcover.

Equations

• compactCoverProperty X K = ∀ (ι : Type ?u.4) (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → K ⊆ ⋃ (i : ι), U i → ∃ (t : Finset ι), K ⊆ ⋃ i ∈ t, U i

theorem compactCoverProperty_iff_isCompact {X : Type u} [PseudoMetricSpace X] {K : Set X} : compactCoverProperty X K ↔ IsCompact K

The book's finite-subcover compactness property agrees with IsCompact.

theorem real_univ_not_compact : ¬IsCompact Set.univ

Example 7.4.8. In ℝ with the standard metric: (i) the whole space ℝ is not compact; (ii) the open interval (0,1) is not compact; (iii) the singleton {0} is compact.

theorem real_Ioo_zero_one_not_compact : ¬IsCompact (Set.Ioo 0 1)

See also: Example 7.4.8 (ii).

theorem real_singleton_zero_compact : IsCompact {0}

See also: Example 7.4.8 (iii).

theorem compact_isClosed {X : Type u} [PseudoMetricSpace X] [T2Space X] {K : Set X} (hK : IsCompact K) : IsClosed K

theorem compact_isBounded {X : Type u} [PseudoMetricSpace X] {K : Set X} (hK : IsCompact K) : Bornology.IsBounded K

theorem compact_isClosed_and_bounded {X : Type u} [PseudoMetricSpace X] [T2Space X] {K : Set X} (hK : IsCompact K) : IsClosed K ∧ Bornology.IsBounded K

Proposition 7.4.9. In a metric space, a compact subset is closed and bounded.

theorem lebesgue_covering_lemma {X : Type u} [PseudoMetricSpace X] {K : Set X} (hseq : ∀ (u : ℕ → X), (∀ (n : ℕ), u n ∈ K) → ∃ l ∈ K, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (u ∘ φ) Filter.atTop (nhds l)) {I : Type v} (U : I → Set X) (hUopen : ∀ (i : I), IsOpen (U i)) (hcover : K ⊆ ⋃ (i : I), U i) : ∃ δ > 0, ∀ x ∈ K, ∃ (i : I), Metric.ball x δ ⊆ U i

Lemma 7.4.10 (Lebesgue covering lemma). If every sequence in a subset K of a metric space has a subsequence converging to a point of K, then for every open cover of K there exists δ > 0 such that every x ∈ K has some open set in the cover containing the ball B(x, δ).

theorem compact_iff_isSeqCompact {X : Type u} [PseudoMetricSpace X] {K : Set X} : IsCompact K ↔ IsSeqCompact K

Theorem 7.4.11. In a metric space, a subset is compact if and only if every sequence in the subset has a subsequence converging to a point of the subset.

theorem real_interval_isSeqCompact (a b : ℝ) : IsSeqCompact (Set.Icc a b)

Example 7.4.12. A closed bounded interval [a,b] ⊆ ℝ is sequentially compact: every sequence in Set.Icc a b admits a convergent subsequence with limit still in the interval.

theorem compact_of_closed_subset {X : Type u} [PseudoMetricSpace X] {K E : Set X} (hK : IsCompact K) (hE : IsClosed E) (hEK : E ⊆ K) : IsCompact E

Proposition 7.4.13. In a metric space, a closed subset of a compact set is compact.

theorem heineBorel_closed_bounded {n : ℕ} {K : Set (EuclideanSpace ℝ (Fin n))} (hclosed : IsClosed K) (hbounded : Bornology.IsBounded K) : IsCompact K

Theorem 7.4.14 (Heine--Borel). A closed bounded subset K ⊆ ℝ^n is compact.

Example 7.4.15. Let X be an infinite set endowed with the discrete metric dist x y = 1 for x ≠ y. Then: (i) the space is complete; (ii) every subset K ⊆ X is closed and bounded; (iii) a subset K is compact if and only if it is finite; (iv) the Lebesgue covering lemma holds for any K with δ = 1/2, even when K is not compact.

theorem discreteMetric_dist_lt_one_iff_eq {X : Type u} [PseudoMetricSpace X] [DecidableEq X] (hdiscrete : ∀ (x y : X), dist x y = if x = y then 0 else 1) {x y : X} : dist x y < 1 ↔ x = y

theorem discreteMetric_ball_eq_singleton {X : Type u} [PseudoMetricSpace X] [DecidableEq X] (hdiscrete : ∀ (x y : X), dist x y = if x = y then 0 else 1) (x : X) {r : ℝ} (hrpos : 0 < r) (hrle : r ≤ 1) : Metric.ball x r = {x}

theorem discreteMetric_cauchySeq_eventually_const {X : Type u} [PseudoMetricSpace X] [DecidableEq X] (hdiscrete : ∀ (x y : X), dist x y = if x = y then 0 else 1) (u : ℕ → X) (hu : CauchySeq u) : ∃ (x0 : X), u =ᶠ[Filter.atTop] fun (x : ℕ) => x0

theorem discreteMetric_complete {X : Type u} [PseudoMetricSpace X] [DecidableEq X] (hdiscrete : ∀ (x y : X), dist x y = if x = y then 0 else 1) : CompleteSpace X

theorem discreteMetric_closed_and_bounded {X : Type u} [PseudoMetricSpace X] [DecidableEq X] (hdiscrete : ∀ (x y : X), dist x y = if x = y then 0 else 1) (hXinf : Infinite X) (K : Set X) : IsClosed K ∧ Bornology.IsBounded K

theorem discreteMetric_compact_iff_finite {X : Type u} [PseudoMetricSpace X] [DecidableEq X] (hdiscrete : ∀ (x y : X), dist x y = if x = y then 0 else 1) (K : Set X) : IsCompact K ↔ K.Finite

theorem discreteMetric_lebesgue_covering {X : Type u} [PseudoMetricSpace X] [DecidableEq X] (hdiscrete : ∀ (x y : X), dist x y = if x = y then 0 else 1) (K : Set X) {I : Type v} (U : I → Set X) (hUopen : ∀ (i : I), IsOpen (U i)) (hcover : K ⊆ ⋃ (i : I), U i) (x : X) : x ∈ K → ∃ (i : I), Metric.ball x (1 / 2) ⊆ U i