@[reducible, inline]

abbrev IsSequentiallyCompact (X : Set ℝ) : Prop

Definition 1.21: A subset X ⊆ ℝ is sequentially compact if every sequence in X has a convergent subsequence whose limit belongs to X.

Equations

• IsSequentiallyCompact X = IsSeqCompact X

theorem isSequentiallyCompact_iff_isSeqCompact (X : Set ℝ) : IsSequentiallyCompact X ↔ IsSeqCompact X

The book's sequential compactness is the same as IsSeqCompact.

theorem heineBorel_real_iff_isSequentiallyCompact (X : Set ℝ) : IsClosed X ∧ Bornology.IsBounded X ↔ IsSequentiallyCompact X

Theorem 1.5 (Heine--Borel theorem on ℝ): For X ⊆ ℝ, the following are equivalent: (i) X is closed and bounded. (ii) Every sequence (x_n) in X has a subsequence (x_{n_k}) converging to a limit x ∈ X.

@[reducible, inline]

abbrev IsSequentiallyCompactSpace (X : Type u_1) [MetricSpace X] : Prop

Definition 1.22 (Compactness): A metric space (X,d) is compact if every sequence (x_n) in X has a strictly increasing k : ℕ → ℕ and a point x ∈ X with d (x_{k(n)}) x → 0. A subset Y ⊆ X is compact in X if the induced metric on Y is compact.

Equations

• IsSequentiallyCompactSpace X = SeqCompactSpace X

@[reducible, inline]

abbrev IsCompactSpace (X : Type u_1) [MetricSpace X] : Prop

Book's compactness of a metric space, expressed as sequential compactness.

Equations

• IsCompactSpace X = IsSequentiallyCompactSpace X

theorem isCompactSpace_iff_seqCompactSpace (X : Type u_1) [MetricSpace X] : IsCompactSpace X ↔ SeqCompactSpace X

The book's compactness of a metric space is equivalent to SeqCompactSpace.

@[reducible, inline]

abbrev IsCompactSubset {X : Type u_1} [MetricSpace X] (Y : Set X) : Prop

Book's compactness for a subset of a metric space, expressed as IsSeqCompact.

Equations

• IsCompactSubset Y = IsSeqCompact Y

theorem isCompactSubset_iff_isSeqCompact {X : Type u_1} [MetricSpace X] (Y : Set X) : IsCompactSubset Y ↔ IsSeqCompact Y

The book's compact subset notion is equivalent to IsSeqCompact.

def IsBoundedSubset {X : Type u_1} [MetricSpace X] (Y : Set X) : Prop

Definition 1.23 (Bounded sets): In a metric space (X,d), a subset Y is bounded if there exist x ∈ X and r ∈ ℝ with 0 ≤ r < ∞ such that Y ⊆ B(x,r) = {y ∈ X : d(x,y) < r}. The metric space (X,d) is bounded if the set X is bounded.

Equations

• IsBoundedSubset Y = (Y = ∅ ∨ ∃ (x : X) (r : ℝ), 0 ≤ r ∧ Y ⊆ Metric.ball x r)

theorem isBoundedSubset_iff_isBounded {X : Type u_1} [MetricSpace X] (Y : Set X) : IsBoundedSubset Y ↔ Bornology.IsBounded Y

The book's boundedness for subsets agrees with Bornology.IsBounded.

@[reducible, inline]

abbrev IsBoundedSpace (X : Type u_1) [MetricSpace X] : Prop

A metric space is bounded if it is a BoundedSpace.

Equations

• IsBoundedSpace X = BoundedSpace X

theorem isBoundedSpace_iff_boundedSpace (X : Type u_1) [MetricSpace X] : IsBoundedSpace X ↔ BoundedSpace X

The book's boundedness of a metric space matches BoundedSpace.

theorem isBoundedSpace_iff_isBounded_univ (X : Type u_1) [MetricSpace X] : IsBoundedSpace X ↔ IsBoundedSubset Set.univ

A metric space is bounded iff its underlying set is bounded in the book's sense.

@[reducible, inline]

abbrev IsCompactOpenCover {X : Type u_1} [MetricSpace X] (K : Set X) : Prop

Definition 1.24: In a metric space (X,d), a subset K ⊆ X is compact if every open cover of K has a finite subcover; i.e. for every family of open sets (U_i)_{i ∈ I} in X with K ⊆ ⋃ i, U_i, there exist indices i₁, …, iₙ ∈ I such that K ⊆ U_{i₁} ∪ … ∪ U_{iₙ}.

Equations

• IsCompactOpenCover K = IsCompact K

theorem isCompactOpenCover_iff_isCompact {X : Type u_1} [MetricSpace X] (K : Set X) : IsCompactOpenCover K ↔ IsCompact K

The book's open-cover compactness for subsets agrees with IsCompact.

@[reducible, inline]

abbrev IsCompactOpenCoverSpace (Y : Type u_1) [TopologicalSpace Y] : Prop

Definition 1.25 (Compactness via open covers): A topological space Y is compact if every open cover of Y has a finite subcover.

Equations

• IsCompactOpenCoverSpace Y = CompactSpace Y

theorem isCompactOpenCoverSpace_iff_compactSpace (Y : Type u_1) [TopologicalSpace Y] : IsCompactOpenCoverSpace Y ↔ CompactSpace Y

The book's open-cover compactness for a space agrees with CompactSpace.

@[reducible, inline]

abbrev IsTotallyBoundedSpace (X : Type u_1) [MetricSpace X] : Prop

Definition 1.26: A metric space (X,d) is totally bounded if for every ε > 0 there exist n ∈ ℕ and points x^(1), …, x^(n) ∈ X such that X = ⋃_{i=1}^n B(x^(i), ε).

Equations

• IsTotallyBoundedSpace X = TotallyBounded Set.univ

theorem isTotallyBoundedSpace_iff_ball_cover (X : Type u_1) [MetricSpace X] : IsTotallyBoundedSpace X ↔ ∀ ε > 0, ∃ (t : Set X), t.Finite ∧ Set.univ ⊆ ⋃ x ∈ t, Metric.ball x ε

The book's totally boundedness is equivalent to a finite cover by metric balls.

theorem helperForProposition_1_28_compactSpace_of_isCompactSpace (X : Type u_1) [MetricSpace X] (hX : IsCompactSpace X) : CompactSpace X

Helper for Proposition 1.28: sequential compactness of the book gives CompactSpace.

theorem helperForProposition_1_28_completeSpace_of_compactSpace (X : Type u_1) [MetricSpace X] [CompactSpace X] : CompleteSpace X

Helper for Proposition 1.28: compact metric spaces are complete.

theorem helperForProposition_1_28_boundedSpace_of_compactSpace (X : Type u_1) [MetricSpace X] [CompactSpace X] : BoundedSpace X

Helper for Proposition 1.28: compact metric spaces are bounded.

theorem compactSpace_complete_and_bounded_prop (X : Type u_1) [MetricSpace X] (hX : IsCompactSpace X) : CompleteSpace X ∧ IsBoundedSpace X

Proposition 1.28: A compact metric space is complete and bounded.

theorem compactSpace_complete_and_bounded (X : Type u_1) [MetricSpace X] (hX : IsCompactSpace X) : CompleteSpace X ∧ IsBoundedSpace X

If a metric space is compact (in the book's sense), then it is complete and bounded.

theorem helperForTheorem_1_6_isClosed {X : Type u_1} [MetricSpace X] {Y : Set X} (hY : IsCompactSubset Y) : IsClosed Y

Helper for Theorem 1.6: a compact subset of a metric space is closed.

theorem compactSubset_closed_and_bounded_prop {X : Type u_1} [MetricSpace X] {Y : Set X} (hY : IsCompactSubset Y) : IsClosed Y ∧ IsBoundedSubset Y

Theorem 1.6: (Compact subsets of metric spaces are closed and bounded) Let (X,d) be a metric space and let Y ⊆ X be compact. Then: (i) Y is closed in X. (ii) Y is bounded, i.e. there exist x₀ ∈ X and R > 0 such that Y ⊆ {x ∈ X : d x x₀ ≤ R}.

theorem compactSubset_closed_and_bounded {X : Type u_1} [MetricSpace X] {Y : Set X} (hY : IsCompactSubset Y) : IsClosed Y ∧ IsBoundedSubset Y

A compact subset of a metric space is closed and bounded.

theorem heineBorel_Rn_iff_isClosed_isBounded_prop (n : ℕ) (E : Set (EuclideanSpace ℝ (Fin n))) : IsCompact E ↔ IsClosed E ∧ Bornology.IsBounded E

Theorem 1.7 (Heine--Borel theorem): Let n ∈ ℕ, and let d be the Euclidean metric, the taxicab metric, or the sup norm metric on ℝ^n. For a set E ⊆ ℝ^n, the following are equivalent: (i) E is compact (every open cover admits a finite subcover). (ii) E is closed and bounded.

theorem heineBorel_Rn_iff_isClosed_isBounded (n : ℕ) (E : Set (EuclideanSpace ℝ (Fin n))) : IsCompact E ↔ IsClosed E ∧ Bornology.IsBounded E

Heine--Borel on ℝ^n: compactness is equivalent to closedness and boundedness.

theorem helperForTheorem_1_8_isCompact {X : Type u_1} [MetricSpace X] {Y : Set X} (hY : IsCompactSubset Y) : IsCompact Y

Helper for Theorem 1.8: sequential compactness of a subset implies compactness.

theorem compactSubset_finite_subcover {X : Type u_1} [MetricSpace X] {Y : Set X} (hY : IsCompactSubset Y) {A : Type u_2} (V : A → Set X) (hV : ∀ (α : A), IsOpen (V α)) (hcover : Y ⊆ ⋃ (α : A), V α) : ∃ (F : Finset A), Y ⊆ ⋃ α ∈ F, V α

Theorem 1.8: Let (X,d) be a metric space, let Y ⊆ X be compact, and let (V_α)_{α∈A} be a family of open subsets of X with Y ⊆ ⋃ α, V α. Then there exists a finite F ⊆ A such that Y ⊆ ⋃ α ∈ F, V α.

theorem helperForTheorem_1_9_isCompact_univ_of_openCover (Y : Type u) [TopologicalSpace Y] (hcover : ∀ {ι : Type u} (U : ι → Set Y), (∀ (i : ι), IsOpen (U i)) → Set.univ ⊆ ⋃ (i : ι), U i → ∃ (s : Finset ι), Set.univ ⊆ ⋃ i ∈ s, U i) : IsCompact Set.univ

Helper for Theorem 1.9: open-cover finite-subcover property implies compactness of Set.univ.

theorem heineBorelProperty_implies_compactSpace (Y : Type u) [TopologicalSpace Y] (hcover : ∀ {ι : Type u} (U : ι → Set Y), (∀ (i : ι), IsOpen (U i)) → Set.univ ⊆ ⋃ (i : ι), U i → ∃ (s : Finset ι), Set.univ ⊆ ⋃ i ∈ s, U i) : CompactSpace Y

Theorem 1.9 (Heine--Borel property implies compactness): Let Y be a topological space. If every open cover of Y admits a finite subcover, then Y is compact.

theorem nested_compact_inter_nonempty {X : Type u_1} [MetricSpace X] (K : ℕ → Set X) (hKcompact : ∀ (n : ℕ), IsCompact (K n)) (hKnonempty : ∀ (n : ℕ), (K n).Nonempty) (hmono : ∀ (n : ℕ), K (n + 1) ⊆ K n) : (⋂ (n : ℕ), K n).Nonempty

Theorem 1.10: Let (K_n)_{n∈ℕ} be a sequence of nonempty compact subsets of a metric space (X,d) such that K_{n+1} ⊆ K_n for all n. Then ⋂ n, K n is nonempty. Nested nonempty compact sets have nonempty intersection.

theorem nested_compact_inter_nonempty_from_one_prop {X : Type u_1} [MetricSpace X] (K : ℕ → Set X) (hKcompact : ∀ (n : ℕ), IsCompact (K n)) (hKnonempty : ∀ (n : ℕ), (K n).Nonempty) (hmono : ∀ (n : ℕ), K (n + 1) ⊆ K n) : (⋂ (n : ℕ), K (n + 1)).Nonempty

Theorem 1.11: For a metric space (X,d) and a nested sequence of nonempty compact subsets K n with K (n+1) ⊆ K n, the intersection ⋂_{n=1}^∞ K_n is nonempty.

theorem nested_compact_inter_nonempty_from_one {X : Type u_1} [MetricSpace X] (K : ℕ → Set X) (hKcompact : ∀ (n : ℕ), IsCompact (K n)) (hKnonempty : ∀ (n : ℕ), (K n).Nonempty) (hmono : ∀ (n : ℕ), K (n + 1) ⊆ K n) : (⋂ (n : ℕ), K (n + 1)).Nonempty

A nested sequence of nonempty compact subsets has nonempty intersection starting at n = 1.

theorem helperForTheorem_1_12_isCompact_univ_subtype {X : Type u_1} [MetricSpace X] {Y : Set X} (hY : IsCompact Y) : IsCompact Set.univ

Helper for Theorem 1.12: compactness of univ in the subtype of a compact set.

theorem compact_basic_properties (X : Type u_1) [MetricSpace X] : (∀ (Y : Set X), IsCompact Y → ∀ (Z : Set ↑Y), IsCompact Z ↔ IsClosed Z) ∧ (∀ {ι : Type u_2} (s : Finset ι) (Y : ι → Set X), (∀ i ∈ s, IsCompact (Y i)) → IsCompact (⋃ i ∈ s, Y i)) ∧ ∀ {Z : Set X}, Z.Finite → IsCompact Z

Theorem 1.12: Let (X,d) be a metric space. (a) If Y ⊆ X is compact and Z ⊆ Y, then Z is compact iff Z is closed in Y. (b) If Y₁, …, Yₙ ⊆ X are compact, then ⋃ i, Yᵢ is compact. (c) Every finite subset of X (including ∅) is compact.

theorem compact_subset_iff_closed_in_compact {X : Type u_1} [MetricSpace X] {Y : Set X} (hY : IsCompact Y) (Z : Set ↑Y) : IsCompact Z ↔ IsClosed Z

Theorem 1.12(a): In a compact subset Y of a metric space, Z ⊆ Y is compact iff it is closed in Y.

theorem compact_iUnion_finset {X : Type u_1} [MetricSpace X] {ι : Type u_2} (s : Finset ι) (Y : ι → Set X) (hY : ∀ i ∈ s, IsCompact (Y i)) : IsCompact (⋃ i ∈ s, Y i)

Theorem 1.12(b): A finite union of compact subsets is compact.

theorem finite_isCompact {X : Type u_1} [MetricSpace X] {Z : Set X} (hZ : Z.Finite) : IsCompact Z

Theorem 1.12(c): Every finite subset of a metric space is compact.

theorem sequentiallyCompactSpace_iff_compactOpenCoverSpace_prop (X : Type u_1) [MetricSpace X] : IsSequentiallyCompactSpace X ↔ IsCompactOpenCoverSpace X

Theorem 1.13 (Equivalence of sequential compactness and open cover compactness): Let (X,d) be a metric space. The following are equivalent: (i) every sequence in X has a convergent subsequence; (ii) every open cover of X has a finite subcover.

theorem sequentiallyCompactSpace_iff_compactOpenCoverSpace (X : Type u_1) [MetricSpace X] : IsSequentiallyCompactSpace X ↔ IsCompactOpenCoverSpace X

In a metric space, sequential compactness is equivalent to open-cover compactness.

def intDiscreteDist (m n : ℤ) : ℝ

Helper for Proposition 1.29: discrete distance on ℤ, 0 on the diagonal and 1 off it.

Equations

• intDiscreteDist m n = if m = n then 0 else 1

theorem intDiscreteDist_self (m : ℤ) : intDiscreteDist m m = 0

Helper for Proposition 1.29: the discrete distance on ℤ is zero on the diagonal.

theorem intDiscreteDist_comm (m n : ℤ) : intDiscreteDist m n = intDiscreteDist n m

Helper for Proposition 1.29: the discrete distance on ℤ is symmetric.

theorem intDiscreteDist_triangle (m n k : ℤ) : intDiscreteDist m k ≤ intDiscreteDist m n + intDiscreteDist n k

Helper for Proposition 1.29: the discrete distance on ℤ satisfies the triangle inequality.

theorem intDiscreteDist_eq_of_dist_eq_zero {m n : ℤ} : intDiscreteDist m n = 0 → m = n

Helper for Proposition 1.29: zero discrete distance on ℤ implies equality.

def intDiscreteMetricSpace : MetricSpace ℤ

Helper for Proposition 1.29: the metric space structure on ℤ induced by intDiscreteDist.

Equations

• One or more equations did not get rendered due to their size.

def instMetricSpaceInt_books : MetricSpace ℤ

Equations

• instMetricSpaceInt_books = intDiscreteMetricSpace

def instDistInt_books : Dist ℤ

Equations

• instDistInt_books = { dist := intDiscreteDist }

def instPseudoMetricSpaceInt_books : PseudoMetricSpace ℤ

Equations

• instPseudoMetricSpaceInt_books = intDiscreteMetricSpace.toPseudoMetricSpace

def instUniformSpaceInt_books : UniformSpace ℤ

Equations

• instUniformSpaceInt_books = PseudoMetricSpace.toUniformSpace

def instTopologicalSpaceInt_books : TopologicalSpace ℤ

Equations

• instTopologicalSpaceInt_books = PseudoMetricSpace.toUniformSpace.toTopologicalSpace

def instBornologyInt_books : Bornology ℤ

Equations

• instBornologyInt_books = PseudoMetricSpace.toBornology

theorem helperForProposition_1_29_eq_of_dist_lt_one_half {m n : ℤ} : intDiscreteDist m n < 1 / 2 → m = n

Helper for Proposition 1.29: in the discrete metric on ℤ, distance < 1/2 forces equality.

theorem helperForProposition_1_29_discreteTopology_intDiscrete : DiscreteTopology ℤ

Helper for Proposition 1.29: the discrete metric on ℤ induces the discrete topology.

theorem helperForProposition_1_29_completeSpace_intDiscrete : CompleteSpace ℤ

Helper for Proposition 1.29: completeness of the discrete metric on ℤ.

theorem helperForProposition_1_29_boundedSpace_intDiscrete : BoundedSpace ℤ

Helper for Proposition 1.29: boundedness of the discrete metric on ℤ.

theorem helperForProposition_1_29_not_compactSpace_intDiscrete : ¬CompactSpace ℤ

Helper for Proposition 1.29: ℤ with the discrete metric is not compact.

theorem int_discreteMetric_complete_bounded_not_compact : CompleteSpace ℤ ∧ BoundedSpace ℤ ∧ ¬CompactSpace ℤ

Proposition 1.29: Let (X,d) be a metric space and equip ℤ with the discrete metric d(m,n)=1 when m ≠ n (and 0 otherwise). Then ℤ is complete and bounded, but not compact.

theorem helperForProposition_1_36_mem_ball_zero_two_intDiscrete (z : ℤ) : z ∈ Metric.ball 0 2

Helper for Proposition 1.36: every integer lies in the ball of radius 2 around 0.

theorem helperForProposition_1_36_isBoundedSubset_univ_intDiscrete : IsBoundedSubset Set.univ

Helper for Proposition 1.36: univ is bounded for the discrete metric on ℤ.

theorem helperForProposition_1_36_not_isCompact_univ_intDiscrete : ¬IsCompact Set.univ

Helper for Proposition 1.36: univ is not compact in the discrete metric on ℤ.

theorem int_discrete_closed_bounded_not_compact : IsClosed Set.univ ∧ IsBoundedSubset Set.univ ∧ ¬IsCompactOpenCover Set.univ

Proposition 1.36: [Heine-Borel fails for discrete metric on ℤ] In the discrete metric on ℤ, the set ℤ is closed and bounded, but not compact. In the discrete metric on ℤ, the whole space is closed and bounded but not compact.