def openBall {X : Type u_1} [PseudoMetricSpace X] (x : X) (δ : ℝ) : Set X

Definition 7.2.1. In a metric space (X, d), the open ball (ball) of radius δ > 0 around x is B(x, δ) = { y ∈ X | d(x, y) < δ }, and the closed ball is C(x, δ) = { y ∈ X | d(x, y) ≤ δ }.

Equations

• openBall x δ = {y : X | dist y x < δ}

def closedBall {X : Type u_1} [PseudoMetricSpace X] (x : X) (δ : ℝ) : Set X

Closed ball with center x and radius δ.

Equations

• closedBall x δ = {y : X | dist y x ≤ δ}

theorem openBall_eq_metric_ball {X : Type u_1} [PseudoMetricSpace X] (x : X) (δ : ℝ) : openBall x δ = Metric.ball x δ

The book's open ball agrees with Metric.ball.

theorem closedBall_eq_metric_closedBall {X : Type u_1} [PseudoMetricSpace X] (x : X) (δ : ℝ) : closedBall x δ = Metric.closedBall x δ

The book's closed ball agrees with Metric.closedBall.

theorem real_openBall_eq_Ioo (x δ : ℝ) : openBall x δ = Set.Ioo (x - δ) (x + δ)

Example 7.2.2. In ℝ with its usual metric, the open ball B(x, δ) of radius δ > 0 around x is the open interval (x - δ, x + δ), and the closed ball C(x, δ) is the closed interval [x - δ, x + δ].

theorem real_closedBall_eq_Icc (x δ : ℝ) : closedBall x δ = Set.Icc (x - δ) (x + δ)

theorem mem_unitInterval_ball_half_iff (y : { y : ℝ // y ∈ Set.Icc 0 1 }) : y ∈ Metric.ball ⟨0, ⋯⟩ (1 / 2) ↔ ↑y < 1 / 2

theorem unitInterval_ball_half : Metric.ball ⟨0, ⋯⟩ (1 / 2) = {y : { y : ℝ // y ∈ Set.Icc 0 1 } | ↑y < 1 / 2}

Example 7.2.3. In the subspace [0, 1] ⊆ ℝ, the open ball of radius 1/2 around 0 consists of those points of [0, 1] whose underlying real coordinate is < 1/2, so it differs from the ambient ball (-1/2, 1/2) ⊆ ℝ.

def IsOpenMetric {X : Type u_1} [PseudoMetricSpace X] (V : Set X) : Prop

Definition 7.2.4. In a metric space (X, d), a subset V ⊆ X is open if for every x ∈ V there exists δ > 0 such that the ball B(x, δ) is contained in V. A subset E ⊆ X is closed if its complement X \ E is open. If x ∈ V and V is open, then V is an open (or simply a) neighborhood of x.

Equations

• IsOpenMetric V = ∀ x ∈ V, ∃ δ > 0, Metric.ball x δ ⊆ V

def IsClosedMetric {X : Type u_1} [PseudoMetricSpace X] (E : Set X) : Prop

A set is closed in the metric sense if its complement is open.

Equations

• IsClosedMetric E = IsOpenMetric Eᶜ

theorem isOpenMetric_iff_isOpen {X : Type u_1} [PseudoMetricSpace X] (V : Set X) : IsOpenMetric V ↔ IsOpen V

The book's notion of an open set agrees with the topological notion coming from the metric space structure.

theorem isClosedMetric_iff_isClosed {X : Type u_1} [PseudoMetricSpace X] (E : Set X) : IsClosedMetric E ↔ IsClosed E

The book's notion of a closed set agrees with IsClosed.

theorem isOpenMetric.mem_nhds {X : Type u_1} [PseudoMetricSpace X] {V : Set X} {x : X} (hV : IsOpenMetric V) (hx : x ∈ V) : V ∈ nhds x

An open set in the metric sense is a neighborhood of each of its points.

theorem real_Ioi_zero_isOpen : IsOpen (Set.Ioi 0)

Example 7.2.5. Basic examples of open and closed subsets of ℝ and singletons in metric spaces: (0, ∞) is open; [0, ∞) is closed; [0, 1) is neither open nor closed; singletons are closed in any metric space, but need not be open (e.g. {0} ⊂ ℝ), while in a one-point metric space {x} is open.

theorem real_Ici_zero_isClosed : IsClosed (Set.Ici 0)

theorem real_Ico_zero_one_not_isOpen : ¬IsOpen (Set.Ico 0 1)

theorem real_Ico_zero_one_not_isClosed : ¬IsClosed (Set.Ico 0 1)

theorem singleton_isClosed {X : Type u_1} [PseudoMetricSpace X] [T1Space X] (x : X) : IsClosed {x}

theorem real_singleton_zero_not_isOpen : ¬IsOpen {0}

theorem singleton_isOpen_of_subsingleton {X : Type u_1} [PseudoMetricSpace X] [Subsingleton X] (x : X) : IsOpen {x}

theorem open_sets_basic {X : Type u_1} [PseudoMetricSpace X] : (IsOpen ∅ ∧ IsOpen Set.univ) ∧ (∀ {ι : Type u_2} (s : Finset ι) (V : ι → Set X), (∀ (i : ι), IsOpen (V i)) → IsOpen (⋂ i ∈ s, V i)) ∧ ∀ {ι : Sort u_3} (V : ι → Set X), (∀ (i : ι), IsOpen (V i)) → IsOpen (⋃ (i : ι), V i)

Proposition 7.2.6. In a metric space (X, d): (i) ∅ and the whole space X are open; (ii) a finite intersection of open sets is open; (iii) an arbitrary union of open sets is open.

theorem iInter_openIntervals_subset_singleton : ⋂ (n : ℕ), Set.Ioo (-(1 / ↑n.succ)) (1 / ↑n.succ) ⊆ {0}

Example 7.2.7. An infinite intersection of open sets need not be open: ⋂ₙ (-1/(n+1), 1/(n+1)) = {0}, so unlike finite intersections, arbitrary intersections of opens may fail to be open.

theorem iInter_openIntervals_eq_singleton : ⋂ (n : ℕ), Set.Ioo (-(1 / ↑n.succ)) (1 / ↑n.succ) = {0}

theorem not_isOpen_iInter_openIntervals : ¬IsOpen (⋂ (n : ℕ), Set.Ioo (-(1 / ↑n.succ)) (1 / ↑n.succ))

theorem closed_sets_basic {X : Type u_1} [PseudoMetricSpace X] : (IsClosed ∅ ∧ IsClosed Set.univ) ∧ (∀ {ι : Sort u_2} (E : ι → Set X), (∀ (i : ι), IsClosed (E i)) → IsClosed (⋂ (i : ι), E i)) ∧ ∀ {ι : Type u_3} (s : Finset ι) (E : ι → Set X), (∀ (i : ι), IsClosed (E i)) → IsClosed (⋃ i ∈ s, E i)

Proposition 7.2.8. In a metric space (X, d): (i) ∅ and X are closed; an arbitrary intersection of closed sets is closed; a finite union of closed sets is closed.

theorem openBall_isOpen_closedBall_isClosed {X : Type u_1} [PseudoMetricSpace X] (x : X) {δ : ℝ} (_hδ : 0 < δ) : IsOpen (openBall x δ) ∧ IsClosed (closedBall x δ)

Proposition 7.2.9. In a metric space (X, d), for any center x and radius δ > 0, the open ball B(x, δ) is open and the closed ball C(x, δ) is closed.

theorem real_intervals_open_closed {a b : ℝ} (_h : a < b) : IsOpen (Set.Ioo a b) ∧ IsOpen (Set.Ioi a) ∧ IsOpen (Set.Iio b) ∧ IsClosed (Set.Icc a b) ∧ IsClosed (Set.Ici a) ∧ IsClosed (Set.Iic b)

Proposition 7.2.10. If a < b in ℝ, then the intervals (a, b), (a, ∞) and (-∞, b) are open in ℝ, while [a, b], [a, ∞) and (-∞, b] are closed in ℝ.

theorem preimage_eq_iff_inter_image_subtype {X : Type u_1} {Y : Set X} (U : Set ↑Y) (V : Set X) : Subtype.val ⁻¹' V = U ↔ V ∩ Y = Subtype.val '' U

theorem subspace_open_exists_open_superset {X : Type u_1} [PseudoMetricSpace X] {Y : Set X} {U : Set ↑Y} : IsOpen U → ∃ (V : Set X), IsOpen V ∧ V ∩ Y = Subtype.val '' U

theorem exists_open_superset_subspace_open {X : Type u_1} [PseudoMetricSpace X] {Y : Set X} {U : Set ↑Y} : (∃ (V : Set X), IsOpen V ∧ V ∩ Y = Subtype.val '' U) → IsOpen U

theorem image_preimage_subtype_eq {X : Type u_1} {V U : Set X} (hUV : U ⊆ V) : Subtype.val '' (Subtype.val ⁻¹' U) = U

theorem subspace_open_iff {X : Type u_1} [PseudoMetricSpace X] {Y : Set X} (U : Set ↑Y) : IsOpen U ↔ ∃ (V : Set X), IsOpen V ∧ V ∩ Y = Subtype.val '' U

Proposition 7.2.11. For a metric space (X, d) and subset Y ⊆ X, a subset U ⊆ Y is open in the subspace topology if and only if there exists an open V ⊆ X with V ∩ Y = U.

theorem open_in_open_subspace_iff {X : Type u_1} [PseudoMetricSpace X] {V U : Set X} (hV : IsOpen V) (hUV : U ⊆ V) : IsOpen (Subtype.val ⁻¹' U) ↔ IsOpen U

Proposition 7.2.12. In a metric space (X, d), if V ⊆ X is open and E ⊆ X is closed, then: (i) a subset U ⊆ V is open in the subspace topology on V iff U is open in X; (ii) a subset F ⊆ E is closed in the subspace topology on E iff F is closed in X.

theorem closed_in_closed_subspace_iff {X : Type u_1} [PseudoMetricSpace X] {E F : Set X} (hE : IsClosed E) (hFE : F ⊆ E) : IsClosed (Subtype.val ⁻¹' F) ↔ IsClosed F

def IsConnectedMetricSpace (X : Type u_1) [PseudoMetricSpace X] : Prop

Definition 7.2.13. A nonempty metric space (X, d) is connected if the only clopen subsets are ∅ and the whole space. A nonempty space that is not connected is called disconnected. A nonempty subset A ⊆ X is connected when it is connected with the subspace topology.

Equations

• IsConnectedMetricSpace X = (Nonempty X ∧ ∀ (V : Set X), IsOpen V → IsClosed V → V = ∅ ∨ V = Set.univ)

theorem isConnectedMetricSpace_iff_connectedSpace (X : Type u_1) [PseudoMetricSpace X] : IsConnectedMetricSpace X ↔ ConnectedSpace X

The book's notion of a connected metric space agrees with ConnectedSpace.

def IsConnectedSubset {X : Type u_1} [PseudoMetricSpace X] (A : Set X) : Prop

A subset is connected in the book's sense when it is connected with the subspace topology.

Equations

• IsConnectedSubset A = IsConnected A

theorem disconnected_iff_exists_open_separation {X : Type u_1} [PseudoMetricSpace X] {S : Set X} (hS : S.Nonempty) : ¬IsConnectedSubset S ↔ ∃ (U₁ : Set X) (U₂ : Set X), IsOpen U₁ ∧ IsOpen U₂ ∧ U₁ ∩ U₂ ∩ S = ∅ ∧ (U₁ ∩ S).Nonempty ∧ (U₂ ∩ S).Nonempty ∧ S = U₁ ∩ S ∪ U₂ ∩ S

Proposition 7.2.14. A nonempty subset S of a metric space is disconnected iff there are open sets U₁ and U₂ in the ambient space such that U₁ ∩ U₂ ∩ S = ∅, both intersections U₁ ∩ S and U₂ ∩ S are nonempty, and S = (U₁ ∩ S) ∪ (U₂ ∩ S).

theorem subset_union_Iio_Ioi_of_not_mem {S : Set ℝ} {z : ℝ} (hz : z ∉ S) : S ⊆ Set.Iio z ∪ Set.Ioi z

A set missing z is contained in the union of (-∞, z) and (z, ∞).

theorem real_set_disconnected_of_gap {S : Set ℝ} {x y z : ℝ} (hx : x ∈ S) (hy : y ∈ S) (hxz : x < z) (hzy : z < y) (hz : z ∉ S) : ¬IsConnectedSubset S

Example 7.2.15. If a set S ⊆ ℝ contains points x and y with x < z < y for some z ∉ S, then S is disconnected, for instance by the separation (-∞, z) and (z, ∞).

theorem real_connected_iff_interval_or_singleton {S : Set ℝ} (hS : S.Nonempty) : IsConnected S ↔ S.OrdConnected ∨ ∃ (x : ℝ), S = {x}

Proposition 7.2.16. A nonempty subset of ℝ is connected if and only if it is an interval or a single point.

noncomputable def discretePseudoMetricSpaceBool : PseudoMetricSpace Bool

Equations

• discretePseudoMetricSpaceBool = PseudoMetricSpace.induced (fun (b : Bool) => if b = true then 1 else 0) inferInstance

noncomputable def instUniformSpaceBool_books : UniformSpace Bool

Equations

• instUniformSpaceBool_books = PseudoMetricSpace.toUniformSpace

noncomputable def instTopologicalSpaceBool_books : TopologicalSpace Bool

Equations

• instTopologicalSpaceBool_books = inferInstance.toTopologicalSpace

theorem discrete_two_point_ball_not_connected : Metric.ball true 2 = Set.univ ∧ ¬IsConnected Set.univ

Example 7.2.17. In a two point space with the discrete metric, the ball of radius 2 around one point is the whole space, which splits into two disjoint open singletons and is therefore not connected.

def closureByClosed {X : Type u_1} [PseudoMetricSpace X] (A : Set X) : Set X

Definition 7.2.18. In a metric space (X, d) and for A ⊆ X, the closure Ā is the intersection of all closed sets containing A.

Equations

• closureByClosed A = ⋂₀ {E : Set X | IsClosed E ∧ A ⊆ E}

theorem closureByClosed_eq_closure {X : Type u_1} [PseudoMetricSpace X] (A : Set X) : closureByClosed A = closure A

The closure defined as the intersection of closed supersets agrees with the topological closure.

theorem closure_properties {X : Type u_1} [PseudoMetricSpace X] (A : Set X) : IsClosed (closure A) ∧ A ⊆ closure A ∧ (IsClosed A → closure A = A)

Proposition 7.2.19. For a subset A of a metric space, the closure Ā is closed and contains A, and if A is already closed then Ā = A.

theorem closure_openInterval_zero_one : closure (Set.Ioo 0 1) = Set.Icc 0 1

Example 7.2.20. The closure of (0, 1) in ℝ is [0, 1].

theorem image_subtype_lt_one_eq_Ioo : Subtype.val '' {x : ↑(Set.Ioi 0) | ↑x < 1} = Set.Ioo 0 1

theorem closure_subtype_rewrite (x : ↑(Set.Ioi 0)) : x ∈ closure {x : ↑(Set.Ioi 0) | ↑x < 1} ↔ ↑x ∈ closure (Set.Ioo 0 1)

theorem mem_target_set_iff_le_one (x : ↑(Set.Ioi 0)) : ↑x ∈ Set.Icc 0 1 ↔ ↑x ≤ 1

theorem closure_Ioo_in_Ioi_eq_Ioc : closure {x : ↑(Set.Ioi 0) | ↑x < 1} = {x : ↑(Set.Ioi 0) | ↑x ≤ 1}

Example 7.2.21. In the ambient metric space (0, ∞), the closure of (0, 1) is (0, 1], since 0 is not available as a limit point but 1 remains a boundary point.

theorem mem_closure_iff_ball_intersects {X : Type u_1} [PseudoMetricSpace X] {A : Set X} {x : X} : x ∈ closure A ↔ ∀ δ > 0, (Metric.ball x δ ∩ A).Nonempty

Proposition 7.2.22. In a metric space (X, d) and subset A ⊆ X, a point x lies in the closure Ā if and only if every open ball around x meets A, that is, B(x, δ) ∩ A ≠ ∅ for all δ > 0.

def metricInterior {X : Type u_1} [PseudoMetricSpace X] (A : Set X) : Set X

Definition 7.2.23. In a metric space (X, d) and a subset A ⊆ X, the interior of A is the set of points x ∈ A for which there exists δ > 0 with B(x, δ) ⊆ A. The boundary of A is ∂A = \overline{A} \setminus Aᵒ.

Equations

• metricInterior A = {x : X | x ∈ A ∧ ∃ δ > 0, Metric.ball x δ ⊆ A}

theorem metricInterior_eq_interior {X : Type u_1} [PseudoMetricSpace X] (A : Set X) : metricInterior A = interior A

The metric description of the interior agrees with the topological interior coming from the metric space structure.

def metricBoundary {X : Type u_1} [PseudoMetricSpace X] (A : Set X) : Set X

The boundary of a subset is its closure minus its interior.

Equations

• metricBoundary A = closure A \ metricInterior A

theorem metricBoundary_eq_frontier {X : Type u_1} [PseudoMetricSpace X] (A : Set X) : metricBoundary A = frontier A

The boundary defined via closure and interior agrees with the topological frontier.

theorem closure_interior_boundary_Ioc_zero_one : closure (Set.Ioc 0 1) = Set.Icc 0 1 ∧ interior (Set.Ioc 0 1) = Set.Ioo 0 1 ∧ frontier (Set.Ioc 0 1) = {0, 1}

Example 7.2.24. For A = (0, 1] ⊆ ℝ, the closure is [0, 1], the interior is (0, 1), and the boundary is {0, 1}.

theorem closure_interior_boundary_discrete_pair : closure {true} = {true} ∧ interior {true} = {true} ∧ frontier {true} = ∅

Example 7.2.25. For the discrete metric on the two-point set X = {a, b} and A = {a}, we have Ā = Aᵒ = A and ∂A = ∅.

theorem interior_open_boundary_closed {X : Type u_1} [PseudoMetricSpace X] (A : Set X) : IsOpen (interior A) ∧ IsClosed (frontier A)

Proposition 7.2.26. In a metric space, the interior of any subset is open and the boundary is closed.

theorem not_mem_interior_iff_ball_meets_compl {X : Type u_1} [PseudoMetricSpace X] {A : Set X} {x : X} : x ∉ interior A ↔ ∀ δ > 0, (Metric.ball x δ ∩ Aᶜ).Nonempty

theorem metricInterior_open_metricBoundary_closed {X : Type u_1} [PseudoMetricSpace X] (A : Set X) : IsOpen (metricInterior A) ∧ IsClosed (metricBoundary A)

Proposition 7.2.26. For a subset A of a metric space, the interior Aᵒ is open and the boundary ∂A is closed.

theorem mem_frontier_iff_ball_intersects {X : Type u_1} [PseudoMetricSpace X] {A : Set X} {x : X} : x ∈ frontier A ↔ ∀ δ > 0, (Metric.ball x δ ∩ A).Nonempty ∧ (Metric.ball x δ ∩ Aᶜ).Nonempty

Proposition 7.2.27. A point x lies in the boundary ∂A of a subset A of a metric space if and only if every open ball around x meets both A and its complement.

theorem frontier_eq_closure_inter_closure_compl {X : Type u_1} [PseudoMetricSpace X] (A : Set X) : frontier A = closure A ∩ closure Aᶜ

Corollary 7.2.28. For a subset A of a metric space, the boundary is the intersection of the closures of A and its complement: ∂A = Ā ∩ \overline{Aᶜ}.