def IsDisconnectedMetricSpace (X : Type u_1) [MetricSpace X] : Prop

A metric space is disconnected if it admits disjoint nonempty open subsets whose union is the whole space.

Equations

• IsDisconnectedMetricSpace X = ∃ (V : Set X) (W : Set X), IsOpen V ∧ IsOpen W ∧ V.Nonempty ∧ W.Nonempty ∧ Disjoint V W ∧ V ∪ W = Set.univ

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

Definition 2.7: [Connected and disconnected metric spaces] Let (X, d) be a metric space. We say that X is disconnected iff there exist disjoint non-empty open sets V and W in X such that V ∪ W = X (equivalently, X contains a non-empty proper subset that is both closed and open). We say that X is connected iff it is non-empty and not disconnected; the empty set is declared neither connected nor disconnected.

Equations

• IsConnectedMetricSpace X = (Nonempty X ∧ ¬IsDisconnectedMetricSpace X)

def IsConnectedSubset (X : Type u_1) [MetricSpace X] (Y : Set X) : Prop

Definition 2.8: [Connected sets] Let (X, d) be a metric space and let Y ⊆ X. Equip Y with the subspace metric. The subset Y is called connected if (Y, d_Y) is connected; it is called disconnected if (Y, d_Y) is disconnected.

Equations

• IsConnectedSubset X Y = IsConnectedMetricSpace (Subtype Y)

def IsDisconnectedSubset (X : Type u_1) [MetricSpace X] (Y : Set X) : Prop

A subset is disconnected when its subtype with the subspace metric is a disconnected metric space.

Equations

• IsDisconnectedSubset X Y = IsDisconnectedMetricSpace (Subtype Y)

theorem helperForTheorem_2_8_isDisconnectedMetricSpace_iff_not_isPreconnected_univ (Y : Type u_1) [MetricSpace Y] : IsDisconnectedMetricSpace Y ↔ ¬IsPreconnected Set.univ

Helper for Theorem 2.8: characterize disconnectedness via preconnectedness of the universe.

theorem helperForTheorem_2_8_isConnectedMetricSpace_iff_isConnected_univ (Y : Type u_1) [MetricSpace Y] : IsConnectedMetricSpace Y ↔ IsConnected Set.univ

Helper for Theorem 2.8: connectedness of a metric space via connectedness of the universal set.

theorem helperForTheorem_2_8_isConnectedSubset_real_iff_isConnected (X : Set ℝ) : IsConnectedSubset ℝ X ↔ IsConnected X

Helper for Theorem 2.8: connectedness of a subset of Real via IsConnected of the set.

theorem helperForTheorem_2_8_isConnected_iff_ordConnected_of_nonempty {X : Set ℝ} (hX : X.Nonempty) : IsConnected X ↔ X.OrdConnected

Helper for Theorem 2.8: on Real, connectedness of a nonempty set is equivalent to order-connectedness.

theorem helperForTheorem_2_8_intervalProperty_lt_iff_ordConnected (X : Set ℝ) : (∀ ⦃x y : ℝ⦄, x ∈ X → y ∈ X → x < y → Set.Icc x y ⊆ X) ↔ X.OrdConnected

Helper for Theorem 2.8: the strict-interval property characterizes order-connectedness.

theorem connected_subset_real_tfae (X : Set ℝ) (hX : X.Nonempty) : [IsConnectedSubset ℝ X, ∀ ⦃x y : ℝ⦄, x ∈ X → y ∈ X → x < y → Set.Icc x y ⊆ X, X.OrdConnected].TFAE

Theorem 2.8: Let X be a nonempty subset of the real line. Then the following statements are equivalent: (a) X is connected; (b) whenever x, y ∈ X and x < y, the interval [x, y] is contained in X; (c) X is an interval.

def IsPathConnectedSubset (X : Type u_1) [MetricSpace X] (E : Set X) : Prop

Definition 2.9: Let (X, d) be a metric space and let E ⊆ X. The set E is path-connected iff for every x, y ∈ E there exists a continuous function γ : [0, 1] → E with γ(0) = x and γ(1) = y.

Equations

• IsPathConnectedSubset X E = IsPathConnected E

theorem helperForTheorem_2_9_isConnectedSubset_iff_isConnected (X : Type u_1) [MetricSpace X] (E : Set X) : IsConnectedSubset X E ↔ IsConnected E

Helper for Theorem 2.9: IsConnectedSubset is equivalent to IsConnected.

theorem helperForTheorem_2_9_isConnected_image_of_continuous {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) {E : Set X} (hE : IsConnected E) : IsConnected (f '' E)

Helper for Theorem 2.9: continuous images preserve connectedness of sets.

theorem continuous_image_connected_subset {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) {E : Set X} (hE : IsConnectedSubset X E) : IsConnectedSubset Y (f '' E)

Theorem 2.9: [Continuity preserves connectedness] Let f : X → Y be continuous between metric spaces. If E is a connected subset of X, then f(E) is a connected subset of Y.

theorem intermediate_value_connected_subset {X : Type u_1} [MetricSpace X] {f : X → ℝ} (hf : Continuous f) {E : Set X} (hE : IsConnectedSubset X E) {a b : X} (ha : a ∈ E) (hb : b ∈ E) {y : ℝ} (hy : f a ≤ y ∧ y ≤ f b ∨ f b ≤ y ∧ y ≤ f a) : ∃ c ∈ E, f c = y

Theorem 2.10: [Intermediate value theorem] Let (X, d_X) be a metric space, let f : X → ℝ be continuous, and let E ⊆ X be connected. For any a, b ∈ E and any y ∈ ℝ satisfying either f(a) ≤ y ≤ f(b) or f(a) ≥ y ≥ f(b), there exists c ∈ E such that f(c) = y.

theorem helperForTheorem_2_11_subtype_eq_of_dist_lt_one_half {X : Type u_1} [MetricSpace X] (hdisc : ∀ (x y : X), dist x y = discreteMetric x y) {E : Set X} {x y : Subtype E} (hxy : dist x y < 1 / 2) : x = y

Helper for Theorem 2.11: in a discrete subspace, points within distance < 1/2 coincide.

theorem helperForTheorem_2_11_isOpen_singleton_subtype {X : Type u_1} [MetricSpace X] (hdisc : ∀ (x y : X), dist x y = discreteMetric x y) {E : Set X} (x : Subtype E) : IsOpen {x}

Helper for Theorem 2.11: singleton subsets of a discrete subspace are open.

theorem discreteMetric_disconnectedSubset_of_two_points {X : Type u_1} [MetricSpace X] (hdisc : ∀ (x y : X), dist x y = discreteMetric x y) {E : Set X} (hE : ∃ x ∈ E, ∃ y ∈ E, x ≠ y) : IsDisconnectedSubset X E

Theorem 2.11: in the discrete metric, any subset with at least two distinct points is disconnected (for the subspace topology).

theorem continuous_iff_constant_of_connected_discrete {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MetricSpace Y] (hX : IsConnectedMetricSpace X) (hdisc : ∀ (y1 y2 : Y), dist y1 y2 = discreteMetric y1 y2) (f : X → Y) : Continuous f ↔ ∀ (x1 x2 : X), f x1 = f x2

Theorem 2.12: Let (X, d) be a connected metric space and let (Y, d_disc) be a metric space equipped with the discrete metric d_disc(y1,y2)=0 if y1=y2 and d_disc(y1,y2)=1 otherwise. For a function f : X → Y, the following are equivalent: (1) f is continuous; (2) f is constant.

theorem connected_subset_of_nonempty_path_connected {X : Type u_1} [MetricSpace X] {E : Set X} (hE_nonempty : E.Nonempty) (hE_path : IsPathConnectedSubset X E) : IsConnectedSubset X E

Proposition 2.20: every non-empty path-connected set in a metric space is connected.

theorem connected_closure_of_path_connected_subset {X : Type u_1} [MetricSpace X] {E : Set X} (hE_nonempty : E.Nonempty) (hE_path : IsPathConnectedSubset X E) : IsConnectedSubset X (closure E)

Theorem 2.13: Let (X, d) be a metric space and let E ⊆ X be nonempty. If E is path-connected, then the closure closure E of E is connected.

theorem connected_closure_of_connected_subset {X : Type u_1} [MetricSpace X] {E : Set X} (hE : IsConnectedSubset X E) : IsConnectedSubset X (closure E)

Proposition 2.21: Let (X, d) be a metric space and let E ⊆ X be connected. Then the closure closure E is connected.

def ConnectedInSubset (X : Type u_1) [MetricSpace X] (x y : X) : Prop

Relation on a metric space given by membership in a common connected subset.

Equations

• ConnectedInSubset X x y = ∃ (C : Set X), IsConnectedSubset X C ∧ x ∈ C ∧ y ∈ C

def ConnectedInSubsetClass (X : Type u_1) [MetricSpace X] (x : X) : Set X

The equivalence class of a point under ConnectedInSubset.

Equations

• ConnectedInSubsetClass X x = {y : X | ConnectedInSubset X x y}

theorem helperForProposition_2_22_connectedInSubset_iff_mem_connectedComponent {X : Type u_1} [MetricSpace X] {x y : X} : ConnectedInSubset X x y ↔ y ∈ connectedComponent x

Helper for Proposition 2.22: ConnectedInSubset matches membership in the connected component.

theorem helperForProposition_2_22_class_eq_connectedComponent {X : Type u_1} [MetricSpace X] (x : X) : ConnectedInSubsetClass X x = connectedComponent x

Helper for Proposition 2.22: the equivalence class equals the connected component.

theorem helperForProposition_2_22_equivalence_connectedInSubset {X : Type u_1} [MetricSpace X] : Equivalence (ConnectedInSubset X)

Helper for Proposition 2.22: ConnectedInSubset is an equivalence relation.

theorem connectedInSubset_equivalence_and_class_connected_closed (X : Type u_1) [MetricSpace X] : Equivalence (ConnectedInSubset X) ∧ ∀ (x : X), IsConnectedSubset X (ConnectedInSubsetClass X x) ∧ IsClosed (ConnectedInSubsetClass X x)

Proposition 2.22: Let (X, d) be a metric space. Define x ∼ y iff there exists a connected subset C ⊆ X with x ∈ C and y ∈ C. Then ∼ is an equivalence relation on X. Moreover, for each x ∈ X, the equivalence class [x] = {y ∈ X : y ∼ x} is connected and closed in X.