doc-next-gen

Mathlib.Topology.Connected.Basic

Module docstring

{"# Connected subsets of topological spaces

In this file we define connected subsets of a topological spaces and various other properties and classes related to connectivity.

Main definitions

We define the following properties for sets in a topological space:

  • IsConnected: a nonempty set that has no non-trivial open partition. See also the section below in the module doc.
  • connectedComponent is the connected component of an element in the space.

We also have a class stating that the whole space satisfies that property: ConnectedSpace

On the definition of connected sets/spaces

In informal mathematics, connected spaces are assumed to be nonempty. We formalise the predicate without that assumption as IsPreconnected. In other words, the only difference is whether the empty space counts as connected. There are good reasons to consider the empty space to be “too simple to be simple” See also https://ncatlab.org/nlab/show/too+simple+to+be+simple, and in particular https://ncatlab.org/nlab/show/too+simple+to+be+simple#relationshiptobiased_definitions. "}

IsPreconnected definition
(s : Set α) : Prop
Full source 
/-- A preconnected set is one where there is no non-trivial open partition. -/
def IsPreconnected (s : Set α) : Prop :=
  ∀ u v : Set α, IsOpen u → IsOpen v → s ⊆ u ∪ v → (s ∩ u).Nonempty → (s ∩ v).Nonempty →
    (s ∩ (u ∩ v)).Nonempty
Preconnected subset of a topological space
Informal description
A subset $s$ of a topological space $\alpha$ is called *preconnected* if for any two open sets $u$ and $v$ such that $s \subseteq u \cup v$, if both $s \cap u$ and $s \cap v$ are nonempty, then $s \cap (u \cap v)$ is also nonempty. In other words, there is no nontrivial open partition of $s$.
IsConnected definition
(s : Set α) : Prop
Full source 
/-- A connected set is one that is nonempty and where there is no non-trivial open partition. -/
def IsConnected (s : Set α) : Prop :=
  s.Nonempty ∧ IsPreconnected s
Connected subset of a topological space
Informal description
A subset $s$ of a topological space $\alpha$ is called *connected* if it is nonempty and for any two open sets $u$ and $v$ such that $s \subseteq u \cup v$, if both $s \cap u$ and $s \cap v$ are nonempty, then $s \cap (u \cap v)$ is also nonempty. In other words, there is no nontrivial open partition of $s$.
IsConnected.nonempty theorem
{s : Set α} (h : IsConnected s) : s.Nonempty
Full source 
theorem IsConnected.nonempty {s : Set α} (h : IsConnected s) : s.Nonempty :=
  h.1
Connected subsets are nonempty
Informal description
For any subset $s$ of a topological space $\alpha$, if $s$ is connected, then $s$ is nonempty.
IsConnected.isPreconnected theorem
{s : Set α} (h : IsConnected s) : IsPreconnected s
Full source 
theorem IsConnected.isPreconnected {s : Set α} (h : IsConnected s) : IsPreconnected s :=
  h.2
Connected subsets are preconnected
Informal description
For any subset $s$ of a topological space $\alpha$, if $s$ is connected, then it is also preconnected. That is, if $s$ is nonempty and has no nontrivial open partition, then it satisfies the weaker condition that there is no nontrivial open partition of $s$ (without requiring nonemptiness).
IsPreirreducible.isPreconnected theorem
{s : Set α} (H : IsPreirreducible s) : IsPreconnected s
Full source 
theorem IsPreirreducible.isPreconnected {s : Set α} (H : IsPreirreducible s) : IsPreconnected s :=
  fun _ _ hu hv _ => H _ _ hu hv
Preirreducible sets are preconnected
Informal description
For any subset $s$ of a topological space $\alpha$, if $s$ is preirreducible, then it is also preconnected. That is, if there are no two disjoint open sets that both intersect $s$ nontrivially, then $s$ cannot be partitioned into two nonempty disjoint open subsets.
IsIrreducible.isConnected theorem
{s : Set α} (H : IsIrreducible s) : IsConnected s
Full source 
theorem IsIrreducible.isConnected {s : Set α} (H : IsIrreducible s) : IsConnected s :=
  ⟨H.nonempty, H.isPreirreducible.isPreconnected⟩
Irreducible sets are connected
Informal description
For any subset $s$ of a topological space $\alpha$, if $s$ is irreducible, then it is connected. That is, if $s$ is nonempty and cannot be covered by two disjoint open sets that both intersect $s$ nontrivially, then $s$ is nonempty and has no nontrivial open partition.
isPreconnected_of_forall theorem
{s : Set α} (x : α) (H : ∀ y ∈ s, ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t) : IsPreconnected s
Full source 
/-- If any point of a set is joined to a fixed point by a preconnected subset,
then the original set is preconnected as well. -/
theorem isPreconnected_of_forall {s : Set α} (x : α)
    (H : ∀ y ∈ s, ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t) : IsPreconnected s := by
  rintro u v hu hv hs ⟨z, zs, zu⟩ ⟨y, ys, yv⟩
  have xs : x ∈ s := by
    rcases H y ys with ⟨t, ts, xt, -, -⟩
    exact ts xt
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: use `wlog xu : x ∈ u := hs xs using u v y z, v u z y`
  cases hs xs with
  | inl xu =>
    rcases H y ys with ⟨t, ts, xt, yt, ht⟩
    have := ht u v hu hv (ts.trans hs) ⟨x, xt, xu⟩ ⟨y, yt, yv⟩
    exact this.imp fun z hz => ⟨ts hz.1, hz.2⟩
  | inr xv =>
    rcases H z zs with ⟨t, ts, xt, zt, ht⟩
    have := ht v u hv hu (ts.trans <| by rwa [union_comm]) ⟨x, xt, xv⟩ ⟨z, zt, zu⟩
    exact this.imp fun _ h => ⟨ts h.1, h.2.2, h.2.1⟩
Preconnectedness via Pointwise Connectedness
Informal description
Let $s$ be a subset of a topological space $\alpha$ and $x \in \alpha$. If for every $y \in s$ there exists a preconnected subset $t \subseteq s$ containing both $x$ and $y$, then $s$ is preconnected.
isPreconnected_of_forall_pair theorem
{s : Set α} (H : ∀ x ∈ s, ∀ y ∈ s, ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t) : IsPreconnected s
Full source 
/-- If any two points of a set are contained in a preconnected subset,
then the original set is preconnected as well. -/
theorem isPreconnected_of_forall_pair {s : Set α}
    (H : ∀ x ∈ s, ∀ y ∈ s, ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t) :
    IsPreconnected s := by
  rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)
  exacts [isPreconnected_empty, isPreconnected_of_forall x fun y => H x hx y]
Preconnectedness via Pairwise Connectedness
Informal description
Let $s$ be a subset of a topological space $\alpha$. If for every pair of points $x, y \in s$, there exists a preconnected subset $t \subseteq s$ containing both $x$ and $y$, then $s$ is preconnected.
isPreconnected_sUnion theorem
(x : α) (c : Set (Set α)) (H1 : ∀ s ∈ c, x ∈ s) (H2 : ∀ s ∈ c, IsPreconnected s) : IsPreconnected (⋃₀ c)
Full source 
/-- A union of a family of preconnected sets with a common point is preconnected as well. -/
theorem isPreconnected_sUnion (x : α) (c : Set (Set α)) (H1 : ∀ s ∈ c, x ∈ s)
    (H2 : ∀ s ∈ c, IsPreconnected s) : IsPreconnected (⋃₀ c) := by
  apply isPreconnected_of_forall x
  rintro y ⟨s, sc, ys⟩
  exact ⟨s, subset_sUnion_of_mem sc, H1 s sc, ys, H2 s sc⟩
Union of Preconnected Sets with Common Point is Preconnected
Informal description
Let $\alpha$ be a topological space, $x \in \alpha$, and $c$ be a family of subsets of $\alpha$ such that: 1. $x$ belongs to every set $s \in c$, 2. Every set $s \in c$ is preconnected. Then the union $\bigcup_{s \in c} s$ is preconnected.
isPreconnected_iUnion theorem
{ι : Sort*} {s : ι → Set α} (h₁ : (⋂ i, s i).Nonempty) (h₂ : ∀ i, IsPreconnected (s i)) : IsPreconnected (⋃ i, s i)
Full source 
theorem isPreconnected_iUnion {ι : Sort*} {s : ι → Set α} (h₁ : (⋂ i, s i).Nonempty)
    (h₂ : ∀ i, IsPreconnected (s i)) : IsPreconnected (⋃ i, s i) :=
  Exists.elim h₁ fun f hf => isPreconnected_sUnion f _ hf (forall_mem_range.2 h₂)
Union of Preconnected Sets with Nonempty Intersection is Preconnected
Informal description
Let $\alpha$ be a topological space and $\{s_i\}_{i \in \iota}$ be a family of subsets of $\alpha$ such that: 1. The intersection $\bigcap_{i \in \iota} s_i$ is nonempty, 2. Each $s_i$ is preconnected. Then the union $\bigcup_{i \in \iota} s_i$ is preconnected.
IsPreconnected.union theorem
(x : α) {s t : Set α} (H1 : x ∈ s) (H2 : x ∈ t) (H3 : IsPreconnected s) (H4 : IsPreconnected t) : IsPreconnected (s ∪ t)
Full source 
theorem IsPreconnected.union (x : α) {s t : Set α} (H1 : x ∈ s) (H2 : x ∈ t) (H3 : IsPreconnected s)
    (H4 : IsPreconnected t) : IsPreconnected (s ∪ t) :=
  sUnion_pair s t ▸ isPreconnected_sUnion x {s, t} (by rintro r (rfl | rfl | h) <;> assumption)
    (by rintro r (rfl | rfl | h) <;> assumption)
Union of Two Preconnected Sets with Common Point is Preconnected
Informal description
Let $\alpha$ be a topological space, $x \in \alpha$, and $s, t \subseteq \alpha$ be two subsets such that: 1. $x \in s$ and $x \in t$, 2. Both $s$ and $t$ are preconnected. Then the union $s \cup t$ is preconnected.
IsPreconnected.union' theorem
{s t : Set α} (H : (s ∩ t).Nonempty) (hs : IsPreconnected s) (ht : IsPreconnected t) : IsPreconnected (s ∪ t)
Full source 
theorem IsPreconnected.union' {s t : Set α} (H : (s ∩ t).Nonempty) (hs : IsPreconnected s)
    (ht : IsPreconnected t) : IsPreconnected (s ∪ t) := by
  rcases H with ⟨x, hxs, hxt⟩
  exact hs.union x hxs hxt ht
Union of Two Preconnected Sets with Nonempty Intersection is Preconnected
Informal description
Let $s$ and $t$ be subsets of a topological space $\alpha$ such that: 1. The intersection $s \cap t$ is nonempty, 2. Both $s$ and $t$ are preconnected. Then the union $s \cup t$ is preconnected.
IsConnected.union theorem
{s t : Set α} (H : (s ∩ t).Nonempty) (Hs : IsConnected s) (Ht : IsConnected t) : IsConnected (s ∪ t)
Full source 
theorem IsConnected.union {s t : Set α} (H : (s ∩ t).Nonempty) (Hs : IsConnected s)
    (Ht : IsConnected t) : IsConnected (s ∪ t) := by
  rcases H with ⟨x, hx⟩
  refine ⟨⟨x, mem_union_left t (mem_of_mem_inter_left hx)⟩, ?_⟩
  exact Hs.isPreconnected.union x (mem_of_mem_inter_left hx) (mem_of_mem_inter_right hx)
    Ht.isPreconnected
Union of Connected Sets with Nonempty Intersection is Connected
Informal description
Let $s$ and $t$ be connected subsets of a topological space $\alpha$ such that their intersection $s \cap t$ is nonempty. Then the union $s \cup t$ is also connected.
IsPreconnected.sUnion_directed theorem
{S : Set (Set α)} (K : DirectedOn (· ⊆ ·) S) (H : ∀ s ∈ S, IsPreconnected s) : IsPreconnected (⋃₀ S)
Full source 
/-- The directed sUnion of a set S of preconnected subsets is preconnected. -/
theorem IsPreconnected.sUnion_directed {S : Set (Set α)} (K : DirectedOn (· ⊆ ·) S)
    (H : ∀ s ∈ S, IsPreconnected s) : IsPreconnected (⋃₀ S) := by
  rintro u v hu hv Huv ⟨a, ⟨s, hsS, has⟩, hau⟩ ⟨b, ⟨t, htS, hbt⟩, hbv⟩
  obtain ⟨r, hrS, hsr, htr⟩ : ∃ r ∈ S, s ⊆ r ∧ t ⊆ r := K s hsS t htS
  have Hnuv : (r ∩ (u ∩ v)).Nonempty :=
    H _ hrS u v hu hv ((subset_sUnion_of_mem hrS).trans Huv) ⟨a, hsr has, hau⟩ ⟨b, htr hbt, hbv⟩
  have Kruv : r ∩ (u ∩ v)r ∩ (u ∩ v) ⊆ ⋃₀ S ∩ (u ∩ v) := inter_subset_inter_left _ (subset_sUnion_of_mem hrS)
  exact Hnuv.mono Kruv
Union of Directed Family of Preconnected Sets is Preconnected
Informal description
Let $S$ be a family of subsets of a topological space $\alpha$ that is directed with respect to the subset relation $\subseteq$. If every subset in $S$ is preconnected, then the union $\bigcup S$ is also preconnected.
IsPreconnected.biUnion_of_reflTransGen theorem
{ι : Type*} {t : Set ι} {s : ι → Set α} (H : ∀ i ∈ t, IsPreconnected (s i)) (K : ∀ i, i ∈ t → ∀ j, j ∈ t → ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j) : IsPreconnected (⋃ n ∈ t, s n)
Full source 
/-- The biUnion of a family of preconnected sets is preconnected if the graph determined by
whether two sets intersect is preconnected. -/
theorem IsPreconnected.biUnion_of_reflTransGen {ι : Type*} {t : Set ι} {s : ι → Set α}
    (H : ∀ i ∈ t, IsPreconnected (s i))
    (K : ∀ i, i ∈ t → ∀ j, j ∈ t → ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j) :
    IsPreconnected (⋃ n ∈ t, s n) := by
  let R := fun i j : ι => (s i ∩ s j).Nonempty ∧ i ∈ t
  have P : ∀ i, i ∈ t → ∀ j, j ∈ t → ReflTransGen R i j →
      ∃ p, p ⊆ t ∧ i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j) := fun i hi j hj h => by
    induction h with
    | refl =>
      refine ⟨{i}, singleton_subset_iff.mpr hi, mem_singleton i, mem_singleton i, ?_⟩
      rw [biUnion_singleton]
      exact H i hi
    | @tail j k _ hjk ih =>
      obtain ⟨p, hpt, hip, hjp, hp⟩ := ih hjk.2
      refine ⟨insert k p, insert_subset_iff.mpr ⟨hj, hpt⟩, mem_insert_of_mem k hip,
        mem_insert k p, ?_⟩
      rw [biUnion_insert]
      refine (H k hj).union' (hjk.1.mono ?_) hp
      rw [inter_comm]
      exact inter_subset_inter_right _ (subset_biUnion_of_mem hjp)
  refine isPreconnected_of_forall_pair ?_
  intro x hx y hy
  obtain ⟨i : ι, hi : i ∈ t, hxi : x ∈ s i⟩ := mem_iUnion₂.1 hx
  obtain ⟨j : ι, hj : j ∈ t, hyj : y ∈ s j⟩ := mem_iUnion₂.1 hy
  obtain ⟨p, hpt, hip, hjp, hp⟩ := P i hi j hj (K i hi j hj)
  exact ⟨⋃ j ∈ p, s j, biUnion_subset_biUnion_left hpt, mem_biUnion hip hxi,
    mem_biUnion hjp hyj, hp⟩
Union of Preconnected Sets with Connected Intersection Graph is Preconnected
Informal description
Let $\alpha$ be a topological space, $\iota$ a type, $t \subseteq \iota$ a subset, and $\{s_i\}_{i \in \iota}$ a family of subsets of $\alpha$. Suppose that: 1. For each $i \in t$, the subset $s_i$ is preconnected. 2. For any $i, j \in t$, the reflexive-transitive closure of the relation "the intersection $s_i \cap s_j$ is nonempty and $i \in t$" connects $i$ to $j$. Then the union $\bigcup_{n \in t} s_n$ is preconnected.
IsConnected.biUnion_of_reflTransGen theorem
{ι : Type*} {t : Set ι} {s : ι → Set α} (ht : t.Nonempty) (H : ∀ i ∈ t, IsConnected (s i)) (K : ∀ i, i ∈ t → ∀ j, j ∈ t → ReflTransGen (fun i j : ι => (s i ∩ s j).Nonempty ∧ i ∈ t) i j) : IsConnected (⋃ n ∈ t, s n)
Full source 
/-- The biUnion of a family of preconnected sets is preconnected if the graph determined by
whether two sets intersect is preconnected. -/
theorem IsConnected.biUnion_of_reflTransGen {ι : Type*} {t : Set ι} {s : ι → Set α}
    (ht : t.Nonempty) (H : ∀ i ∈ t, IsConnected (s i))
    (K : ∀ i, i ∈ t → ∀ j, j ∈ t → ReflTransGen (fun i j : ι => (s i ∩ s j).Nonempty ∧ i ∈ t) i j) :
    IsConnected (⋃ n ∈ t, s n) :=
  ⟨nonempty_biUnion.2 <| ⟨ht.some, ht.some_mem, (H _ ht.some_mem).nonempty⟩,
    IsPreconnected.biUnion_of_reflTransGen (fun i hi => (H i hi).isPreconnected) K⟩
Union of Connected Sets with Connected Intersection Graph is Connected
Informal description
Let $\alpha$ be a topological space, $\iota$ a type, and $t \subseteq \iota$ a nonempty subset. Consider a family of subsets $\{s_i\}_{i \in \iota}$ of $\alpha$ such that: 1. For each $i \in t$, the subset $s_i$ is connected. 2. For any $i, j \in t$, the reflexive-transitive closure of the relation "$s_i \cap s_j$ is nonempty and $i \in t$" connects $i$ to $j$. Then the union $\bigcup_{n \in t} s_n$ is connected.
IsPreconnected.iUnion_of_reflTransGen theorem
{ι : Type*} {s : ι → Set α} (H : ∀ i, IsPreconnected (s i)) (K : ∀ i j, ReflTransGen (fun i j : ι => (s i ∩ s j).Nonempty) i j) : IsPreconnected (⋃ n, s n)
Full source 
/-- Preconnectedness of the iUnion of a family of preconnected sets
indexed by the vertices of a preconnected graph,
where two vertices are joined when the corresponding sets intersect. -/
theorem IsPreconnected.iUnion_of_reflTransGen {ι : Type*} {s : ι → Set α}
    (H : ∀ i, IsPreconnected (s i))
    (K : ∀ i j, ReflTransGen (fun i j : ι => (s i ∩ s j).Nonempty) i j) :
    IsPreconnected (⋃ n, s n) := by
  rw [← biUnion_univ]
  exact IsPreconnected.biUnion_of_reflTransGen (fun i _ => H i) fun i _ j _ => by
    simpa [mem_univ] using K i j
Union of Preconnected Sets with Connected Intersection Graph is Preconnected
Informal description
Let $\alpha$ be a topological space, $\iota$ a type, and $\{s_i\}_{i \in \iota}$ a family of subsets of $\alpha$. Suppose that: 1. For each $i \in \iota$, the subset $s_i$ is preconnected. 2. For any $i, j \in \iota$, the reflexive-transitive closure of the relation "$s_i \cap s_j$ is nonempty" connects $i$ to $j$. Then the union $\bigcup_{n} s_n$ is preconnected.
IsConnected.iUnion_of_reflTransGen theorem
{ι : Type*} [Nonempty ι] {s : ι → Set α} (H : ∀ i, IsConnected (s i)) (K : ∀ i j, ReflTransGen (fun i j : ι => (s i ∩ s j).Nonempty) i j) : IsConnected (⋃ n, s n)
Full source 
theorem IsConnected.iUnion_of_reflTransGen {ι : Type*} [Nonempty ι] {s : ι → Set α}
    (H : ∀ i, IsConnected (s i))
    (K : ∀ i j, ReflTransGen (fun i j : ι => (s i ∩ s j).Nonempty) i j) : IsConnected (⋃ n, s n) :=
  ⟨nonempty_iUnion.2 <| Nonempty.elim ‹_› fun i : ι => ⟨i, (H _).nonempty⟩,
    IsPreconnected.iUnion_of_reflTransGen (fun i => (H i).isPreconnected) K⟩
Union of Connected Sets with Connected Intersection Graph is Connected
Informal description
Let $\alpha$ be a topological space, $\iota$ a nonempty type, and $\{s_i\}_{i \in \iota}$ a family of subsets of $\alpha$. Suppose that: 1. For each $i \in \iota$, the subset $s_i$ is connected. 2. For any $i, j \in \iota$, the reflexive-transitive closure of the relation "$s_i \cap s_j$ is nonempty" connects $i$ to $j$. Then the union $\bigcup_{n} s_n$ is connected.
IsPreconnected.iUnion_of_chain theorem
{s : β → Set α} (H : ∀ n, IsPreconnected (s n)) (K : ∀ n, (s n ∩ s (succ n)).Nonempty) : IsPreconnected (⋃ n, s n)
Full source 
/-- The iUnion of connected sets indexed by a type with an archimedean successor (like `ℕ` or `ℤ`)
  such that any two neighboring sets meet is preconnected. -/
theorem IsPreconnected.iUnion_of_chain {s : β → Set α} (H : ∀ n, IsPreconnected (s n))
    (K : ∀ n, (s n ∩ s (succ n)).Nonempty) : IsPreconnected (⋃ n, s n) :=
  IsPreconnected.iUnion_of_reflTransGen H fun _ _ =>
    reflTransGen_of_succ _ (fun i _ => K i) fun i _ => by
      rw [inter_comm]
      exact K i
Union of Preconnected Sets Along a Successor Chain is Preconnected
Informal description
Let $\alpha$ be a topological space and $\beta$ a type with a successor function. Given a family of subsets $\{s_n\}_{n \in \beta}$ of $\alpha$ such that: 1. Each $s_n$ is preconnected. 2. For every $n \in \beta$, the intersection $s_n \cap s_{\text{succ}(n)}$ is nonempty. Then the union $\bigcup_{n} s_n$ is preconnected.
IsConnected.iUnion_of_chain theorem
[Nonempty β] {s : β → Set α} (H : ∀ n, IsConnected (s n)) (K : ∀ n, (s n ∩ s (succ n)).Nonempty) : IsConnected (⋃ n, s n)
Full source 
/-- The iUnion of connected sets indexed by a type with an archimedean successor (like `ℕ` or `ℤ`)
  such that any two neighboring sets meet is connected. -/
theorem IsConnected.iUnion_of_chain [Nonempty β] {s : β → Set α} (H : ∀ n, IsConnected (s n))
    (K : ∀ n, (s n ∩ s (succ n)).Nonempty) : IsConnected (⋃ n, s n) :=
  IsConnected.iUnion_of_reflTransGen H fun _ _ =>
    reflTransGen_of_succ _ (fun i _ => K i) fun i _ => by
      rw [inter_comm]
      exact K i
Union of Connected Sets Along a Successor Chain is Connected
Informal description
Let $\alpha$ be a topological space and $\beta$ a nonempty type with a successor function. Given a family of connected subsets $\{s_n\}_{n \in \beta}$ of $\alpha$ such that for each $n \in \beta$, the intersection $s_n \cap s_{\text{succ}(n)}$ is nonempty, then the union $\bigcup_{n} s_n$ is connected.
IsPreconnected.biUnion_of_chain theorem
{s : β → Set α} {t : Set β} (ht : OrdConnected t) (H : ∀ n ∈ t, IsPreconnected (s n)) (K : ∀ n : β, n ∈ t → succ n ∈ t → (s n ∩ s (succ n)).Nonempty) : IsPreconnected (⋃ n ∈ t, s n)
Full source 
/-- The iUnion of preconnected sets indexed by a subset of a type with an archimedean successor
  (like `ℕ` or `ℤ`) such that any two neighboring sets meet is preconnected. -/
theorem IsPreconnected.biUnion_of_chain {s : β → Set α} {t : Set β} (ht : OrdConnected t)
    (H : ∀ n ∈ t, IsPreconnected (s n))
    (K : ∀ n : β, n ∈ t → succsucc n ∈ t → (s n ∩ s (succ n)).Nonempty) :
    IsPreconnected (⋃ n ∈ t, s n) := by
  have h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t := fun hi hj hk =>
    ht.out hi hj (Ico_subset_Icc_self hk)
  have h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succsucc k ∈ t := fun hi hj hk =>
    ht.out hi hj ⟨hk.1.trans <| le_succ _, succ_le_of_lt hk.2⟩
  have h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty :=
    fun hi hj hk => K _ (h1 hi hj hk) (h2 hi hj hk)
  refine IsPreconnected.biUnion_of_reflTransGen H fun i hi j hj => ?_
  exact reflTransGen_of_succ _ (fun k hk => ⟨h3 hi hj hk, h1 hi hj hk⟩) fun k hk =>
      ⟨by rw [inter_comm]; exact h3 hj hi hk, h2 hj hi hk⟩
Union of Preconnected Sets Along a Chain is Preconnected
Informal description
Let $\alpha$ be a topological space, $\beta$ a type with a successor function, $t \subseteq \beta$ an order-connected subset, and $\{s_n\}_{n \in \beta}$ a family of subsets of $\alpha$. Suppose that: 1. For each $n \in t$, the subset $s_n$ is preconnected. 2. For any $n \in t$ such that $\text{succ}(n) \in t$, the intersection $s_n \cap s_{\text{succ}(n)}$ is nonempty. Then the union $\bigcup_{n \in t} s_n$ is preconnected.
IsConnected.biUnion_of_chain theorem
{s : β → Set α} {t : Set β} (hnt : t.Nonempty) (ht : OrdConnected t) (H : ∀ n ∈ t, IsConnected (s n)) (K : ∀ n : β, n ∈ t → succ n ∈ t → (s n ∩ s (succ n)).Nonempty) : IsConnected (⋃ n ∈ t, s n)
Full source 
/-- The iUnion of connected sets indexed by a subset of a type with an archimedean successor
  (like `ℕ` or `ℤ`) such that any two neighboring sets meet is preconnected. -/
theorem IsConnected.biUnion_of_chain {s : β → Set α} {t : Set β} (hnt : t.Nonempty)
    (ht : OrdConnected t) (H : ∀ n ∈ t, IsConnected (s n))
    (K : ∀ n : β, n ∈ t → succsucc n ∈ t → (s n ∩ s (succ n)).Nonempty) : IsConnected (⋃ n ∈ t, s n) :=
  ⟨nonempty_biUnion.2 <| ⟨hnt.some, hnt.some_mem, (H _ hnt.some_mem).nonempty⟩,
    IsPreconnected.biUnion_of_chain ht (fun i hi => (H i hi).isPreconnected) K⟩
Union of Connected Sets Along a Chain is Connected
Informal description
Let $\alpha$ be a topological space and $\beta$ a type with a successor function. Given a nonempty order-connected subset $t \subseteq \beta$ and a family of subsets $\{s_n\}_{n \in \beta}$ of $\alpha$ such that: 1. For each $n \in t$, the subset $s_n$ is connected. 2. For any $n \in t$ with $\text{succ}(n) \in t$, the intersection $s_n \cap s_{\text{succ}(n)}$ is nonempty. Then the union $\bigcup_{n \in t} s_n$ is connected.
IsPreconnected.subset_closure theorem
{s : Set α} {t : Set α} (H : IsPreconnected s) (Kst : s ⊆ t) (Ktcs : t ⊆ closure s) : IsPreconnected t
Full source 
/-- Theorem of bark and tree: if a set is within a preconnected set and its closure, then it is
preconnected as well. See also `IsConnected.subset_closure`. -/
protected theorem IsPreconnected.subset_closure {s : Set α} {t : Set α} (H : IsPreconnected s)
    (Kst : s ⊆ t) (Ktcs : t ⊆ closure s) : IsPreconnected t :=
  fun u v hu hv htuv ⟨_y, hyt, hyu⟩ ⟨_z, hzt, hzv⟩ =>
  let ⟨p, hpu, hps⟩ := mem_closure_iff.1 (Ktcs hyt) u hu hyu
  let ⟨q, hqv, hqs⟩ := mem_closure_iff.1 (Ktcs hzt) v hv hzv
  let ⟨r, hrs, hruv⟩ := H u v hu hv (Subset.trans Kst htuv) ⟨p, hps, hpu⟩ ⟨q, hqs, hqv⟩
  ⟨r, Kst hrs, hruv⟩
Preconnectedness is preserved under closure inclusion
Informal description
Let $s$ and $t$ be subsets of a topological space $\alpha$. If $s$ is preconnected, $s \subseteq t$, and $t$ is contained in the closure of $s$, then $t$ is also preconnected.
IsConnected.subset_closure theorem
{s : Set α} {t : Set α} (H : IsConnected s) (Kst : s ⊆ t) (Ktcs : t ⊆ closure s) : IsConnected t
Full source 
/-- Theorem of bark and tree: if a set is within a connected set and its closure, then it is
connected as well. See also `IsPreconnected.subset_closure`. -/
protected theorem IsConnected.subset_closure {s : Set α} {t : Set α} (H : IsConnected s)
    (Kst : s ⊆ t) (Ktcs : t ⊆ closure s) : IsConnected t :=
  ⟨Nonempty.mono Kst H.left, IsPreconnected.subset_closure H.right Kst Ktcs⟩
Connectedness is preserved under closure inclusion
Informal description
Let $s$ and $t$ be subsets of a topological space $\alpha$. If $s$ is connected, $s \subseteq t$, and $t$ is contained in the closure of $s$, then $t$ is also connected.
IsPreconnected.closure theorem
{s : Set α} (H : IsPreconnected s) : IsPreconnected (closure s)
Full source 
/-- The closure of a preconnected set is preconnected as well. -/
protected theorem IsPreconnected.closure {s : Set α} (H : IsPreconnected s) :
    IsPreconnected (closure s) :=
  IsPreconnected.subset_closure H subset_closure Subset.rfl
Preconnectedness is preserved under closure
Informal description
If a subset $s$ of a topological space $\alpha$ is preconnected, then its closure $\overline{s}$ is also preconnected.
IsPreconnected.image theorem
[TopologicalSpace β] {s : Set α} (H : IsPreconnected s) (f : α → β) (hf : ContinuousOn f s) : IsPreconnected (f '' s)
Full source 
/-- The image of a preconnected set is preconnected as well. -/
protected theorem IsPreconnected.image [TopologicalSpace β] {s : Set α} (H : IsPreconnected s)
    (f : α → β) (hf : ContinuousOn f s) : IsPreconnected (f '' s) := by
  -- Unfold/destruct definitions in hypotheses
  rintro u v hu hv huv ⟨_, ⟨x, xs, rfl⟩, xu⟩ ⟨_, ⟨y, ys, rfl⟩, yv⟩
  rcases continuousOn_iff'.1 hf u hu with ⟨u', hu', u'_eq⟩
  rcases continuousOn_iff'.1 hf v hv with ⟨v', hv', v'_eq⟩
  -- Reformulate `huv : f '' s ⊆ u ∪ v` in terms of `u'` and `v'`
  replace huv : s ⊆ u' ∪ v' := by
    rw [image_subset_iff, preimage_union] at huv
    replace huv := subset_inter huv Subset.rfl
    rw [union_inter_distrib_right, u'_eq, v'_eq, ← union_inter_distrib_right] at huv
    exact (subset_inter_iff.1 huv).1
  -- Now `s ⊆ u' ∪ v'`, so we can apply `‹IsPreconnected s›`
  obtain ⟨z, hz⟩ : (s ∩ (u' ∩ v')).Nonempty := by
    refine H u' v' hu' hv' huv ⟨x, ?_⟩ ⟨y, ?_⟩ <;> rw [inter_comm]
    exacts [u'_eq ▸ ⟨xu, xs⟩, v'_eq ▸ ⟨yv, ys⟩]
  rw [← inter_self s, inter_assoc, inter_left_comm s u', ← inter_assoc, inter_comm s, inter_comm s,
    ← u'_eq, ← v'_eq] at hz
  exact ⟨f z, ⟨z, hz.1.2, rfl⟩, hz.1.1, hz.2.1⟩
Continuous Image of a Preconnected Set is Preconnected
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a preconnected subset, and $f \colon X \to Y$ a continuous function on $s$. Then the image $f(s)$ is also preconnected.
IsConnected.image theorem
[TopologicalSpace β] {s : Set α} (H : IsConnected s) (f : α → β) (hf : ContinuousOn f s) : IsConnected (f '' s)
Full source 
/-- The image of a connected set is connected as well. -/
protected theorem IsConnected.image [TopologicalSpace β] {s : Set α} (H : IsConnected s) (f : α → β)
    (hf : ContinuousOn f s) : IsConnected (f '' s) :=
  ⟨image_nonempty.mpr H.nonempty, H.isPreconnected.image f hf⟩
Continuous Image of a Connected Set is Connected
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a connected subset, and $f \colon X \to Y$ a continuous function on $s$. Then the image $f(s)$ is also connected.
isPreconnected_closed_iff theorem
{s : Set α} : IsPreconnected s ↔ ∀ t t', IsClosed t → IsClosed t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
Full source 
theorem isPreconnected_closed_iff {s : Set α} :
    IsPreconnectedIsPreconnected s ↔ ∀ t t', IsClosed t → IsClosed t' →
      s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty :=
  ⟨by
      rintro h t t' ht ht' htt' ⟨x, xs, xt⟩ ⟨y, ys, yt'⟩
      rw [← not_disjoint_iff_nonempty_inter, ← subset_compl_iff_disjoint_right, compl_inter]
      intro h'
      have xt' : x ∉ t' := (h' xs).resolve_left (absurd xt)
      have yt : y ∉ t := (h' ys).resolve_right (absurd yt')
      have := h _ _ ht.isOpen_compl ht'.isOpen_compl h' ⟨y, ys, yt⟩ ⟨x, xs, xt'⟩
      rw [← compl_union] at this
      exact this.ne_empty htt'.disjoint_compl_right.inter_eq,
    by
      rintro h u v hu hv huv ⟨x, xs, xu⟩ ⟨y, ys, yv⟩
      rw [← not_disjoint_iff_nonempty_inter, ← subset_compl_iff_disjoint_right, compl_inter]
      intro h'
      have xv : x ∉ v := (h' xs).elim (absurd xu) id
      have yu : y ∉ u := (h' ys).elim id (absurd yv)
      have := h _ _ hu.isClosed_compl hv.isClosed_compl h' ⟨y, ys, yu⟩ ⟨x, xs, xv⟩
      rw [← compl_union] at this
      exact this.ne_empty huv.disjoint_compl_right.inter_eq⟩
Characterization of Preconnected Sets via Closed Covers
Informal description
A subset $s$ of a topological space $\alpha$ is preconnected if and only if for any two closed sets $t$ and $t'$ such that $s \subseteq t \cup t'$, if both $s \cap t$ and $s \cap t'$ are nonempty, then $s \cap (t \cap t')$ is also nonempty.
Topology.IsInducing.isPreconnected_image theorem
[TopologicalSpace β] {s : Set α} {f : α → β} (hf : IsInducing f) : IsPreconnected (f '' s) ↔ IsPreconnected s
Full source 
theorem Topology.IsInducing.isPreconnected_image [TopologicalSpace β] {s : Set α} {f : α → β}
    (hf : IsInducing f) : IsPreconnectedIsPreconnected (f '' s) ↔ IsPreconnected s := by
  refine ⟨fun h => ?_, fun h => h.image _ hf.continuous.continuousOn⟩
  rintro u v hu' hv' huv ⟨x, hxs, hxu⟩ ⟨y, hys, hyv⟩
  rcases hf.isOpen_iff.1 hu' with ⟨u, hu, rfl⟩
  rcases hf.isOpen_iff.1 hv' with ⟨v, hv, rfl⟩
  replace huv : f '' sf '' s ⊆ u ∪ v := by rwa [image_subset_iff]
  rcases h u v hu hv huv ⟨f x, mem_image_of_mem _ hxs, hxu⟩ ⟨f y, mem_image_of_mem _ hys, hyv⟩ with
    ⟨_, ⟨z, hzs, rfl⟩, hzuv⟩
  exact ⟨z, hzs, hzuv⟩
Preconnectedness of Image under Inducing Map iff Preconnectedness of Domain
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a subset, and $f \colon X \to Y$ an inducing map. Then the image $f(s)$ is preconnected in $Y$ if and only if $s$ is preconnected in $X$.
IsPreconnected.preimage_of_isOpenMap theorem
[TopologicalSpace β] {f : α → β} {s : Set β} (hs : IsPreconnected s) (hinj : Function.Injective f) (hf : IsOpenMap f) (hsf : s ⊆ range f) : IsPreconnected (f ⁻¹' s)
Full source 
theorem IsPreconnected.preimage_of_isOpenMap [TopologicalSpace β] {f : α → β} {s : Set β}
    (hs : IsPreconnected s) (hinj : Function.Injective f) (hf : IsOpenMap f) (hsf : s ⊆ range f) :
    IsPreconnected (f ⁻¹' s) := fun u v hu hv hsuv hsu hsv => by
  replace hsf : f '' (f ⁻¹' s) = s := image_preimage_eq_of_subset hsf
  obtain ⟨_, has, ⟨a, hau, rfl⟩, hav⟩ : (s ∩ (f '' u ∩ f '' v)).Nonempty := by
    refine hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_
    · simpa only [hsf, image_union] using image_subset f hsuv
    · simpa only [image_preimage_inter] using hsu.image f
    · simpa only [image_preimage_inter] using hsv.image f
  · exact ⟨a, has, hau, hinj.mem_set_image.1 hav⟩
Preimage of Preconnected Set under Injective Open Map is Preconnected
Informal description
Let $f \colon \alpha \to \beta$ be an injective open map between topological spaces, and let $s \subseteq \beta$ be a preconnected subset contained in the range of $f$. Then the preimage $f^{-1}(s)$ is also preconnected.
IsPreconnected.preimage_of_isClosedMap theorem
[TopologicalSpace β] {s : Set β} (hs : IsPreconnected s) {f : α → β} (hinj : Function.Injective f) (hf : IsClosedMap f) (hsf : s ⊆ range f) : IsPreconnected (f ⁻¹' s)
Full source 
theorem IsPreconnected.preimage_of_isClosedMap [TopologicalSpace β] {s : Set β}
    (hs : IsPreconnected s) {f : α → β} (hinj : Function.Injective f) (hf : IsClosedMap f)
    (hsf : s ⊆ range f) : IsPreconnected (f ⁻¹' s) :=
  isPreconnected_closed_iff.2 fun u v hu hv hsuv hsu hsv => by
    replace hsf : f '' (f ⁻¹' s) = s := image_preimage_eq_of_subset hsf
    obtain ⟨_, has, ⟨a, hau, rfl⟩, hav⟩ : (s ∩ (f '' u ∩ f '' v)).Nonempty := by
      refine isPreconnected_closed_iff.1 hs (f '' u) (f '' v) (hf u hu) (hf v hv) ?_ ?_ ?_
      · simpa only [hsf, image_union] using image_subset f hsuv
      · simpa only [image_preimage_inter] using hsu.image f
      · simpa only [image_preimage_inter] using hsv.image f
    · exact ⟨a, has, hau, hinj.mem_set_image.1 hav⟩
Preimage of Preconnected Set under Injective Closed Map is Preconnected
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq Y$ a preconnected subset, and $f : X \to Y$ an injective closed map such that $s$ is contained in the range of $f$. Then the preimage $f^{-1}(s)$ is preconnected in $X$.
IsConnected.preimage_of_isOpenMap theorem
[TopologicalSpace β] {s : Set β} (hs : IsConnected s) {f : α → β} (hinj : Function.Injective f) (hf : IsOpenMap f) (hsf : s ⊆ range f) : IsConnected (f ⁻¹' s)
Full source 
theorem IsConnected.preimage_of_isOpenMap [TopologicalSpace β] {s : Set β} (hs : IsConnected s)
    {f : α → β} (hinj : Function.Injective f) (hf : IsOpenMap f) (hsf : s ⊆ range f) :
    IsConnected (f ⁻¹' s) :=
  ⟨hs.nonempty.preimage' hsf, hs.isPreconnected.preimage_of_isOpenMap hinj hf hsf⟩
Preimage of Connected Set under Injective Open Map is Connected
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq Y$ a connected subset, and $f : X \to Y$ an injective open map such that $s$ is contained in the range of $f$. Then the preimage $f^{-1}(s)$ is connected in $X$.
IsConnected.preimage_of_isClosedMap theorem
[TopologicalSpace β] {s : Set β} (hs : IsConnected s) {f : α → β} (hinj : Function.Injective f) (hf : IsClosedMap f) (hsf : s ⊆ range f) : IsConnected (f ⁻¹' s)
Full source 
theorem IsConnected.preimage_of_isClosedMap [TopologicalSpace β] {s : Set β} (hs : IsConnected s)
    {f : α → β} (hinj : Function.Injective f) (hf : IsClosedMap f) (hsf : s ⊆ range f) :
    IsConnected (f ⁻¹' s) :=
  ⟨hs.nonempty.preimage' hsf, hs.isPreconnected.preimage_of_isClosedMap hinj hf hsf⟩
Preimage of Connected Set under Injective Closed Map is Connected
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq Y$ a connected subset, and $f \colon X \to Y$ an injective closed map such that $s$ is contained in the range of $f$. Then the preimage $f^{-1}(s)$ is connected in $X$.
IsPreconnected.subset_or_subset theorem
(hu : IsOpen u) (hv : IsOpen v) (huv : Disjoint u v) (hsuv : s ⊆ u ∪ v) (hs : IsPreconnected s) : s ⊆ u ∨ s ⊆ v
Full source 
theorem IsPreconnected.subset_or_subset (hu : IsOpen u) (hv : IsOpen v) (huv : Disjoint u v)
    (hsuv : s ⊆ u ∪ v) (hs : IsPreconnected s) : s ⊆ us ⊆ u ∨ s ⊆ v := by
  specialize hs u v hu hv hsuv
  obtain hsu | hsu := (s ∩ u).eq_empty_or_nonempty
  · exact Or.inr ((Set.disjoint_iff_inter_eq_empty.2 hsu).subset_right_of_subset_union hsuv)
  · replace hs := mt (hs hsu)
    simp_rw [Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty,
      disjoint_iff_inter_eq_empty.1 huv] at hs
    exact Or.inl ((hs s.disjoint_empty).subset_left_of_subset_union hsuv)
Preconnected Sets are Indecomposable by Disjoint Open Covers
Informal description
Let $X$ be a topological space and $s \subseteq X$ be a preconnected subset. For any two disjoint open sets $u$ and $v$ in $X$ such that $s \subseteq u \cup v$, either $s \subseteq u$ or $s \subseteq v$.
IsPreconnected.subset_left_of_subset_union theorem
(hu : IsOpen u) (hv : IsOpen v) (huv : Disjoint u v) (hsuv : s ⊆ u ∪ v) (hsu : (s ∩ u).Nonempty) (hs : IsPreconnected s) : s ⊆ u
Full source 
theorem IsPreconnected.subset_left_of_subset_union (hu : IsOpen u) (hv : IsOpen v)
    (huv : Disjoint u v) (hsuv : s ⊆ u ∪ v) (hsu : (s ∩ u).Nonempty) (hs : IsPreconnected s) :
    s ⊆ u :=
  Disjoint.subset_left_of_subset_union hsuv
    (by
      by_contra hsv
      rw [not_disjoint_iff_nonempty_inter] at hsv
      obtain ⟨x, _, hx⟩ := hs u v hu hv hsuv hsu hsv
      exact Set.disjoint_iff.1 huv hx)
Preconnected Subset Contained in One Component of Open Partition
Informal description
Let $s$ be a preconnected subset of a topological space, and let $u$ and $v$ be two disjoint open sets such that $s \subseteq u \cup v$. If $s$ has a nonempty intersection with $u$, then $s$ is entirely contained in $u$.
IsPreconnected.subset_right_of_subset_union theorem
(hu : IsOpen u) (hv : IsOpen v) (huv : Disjoint u v) (hsuv : s ⊆ u ∪ v) (hsv : (s ∩ v).Nonempty) (hs : IsPreconnected s) : s ⊆ v
Full source 
theorem IsPreconnected.subset_right_of_subset_union (hu : IsOpen u) (hv : IsOpen v)
    (huv : Disjoint u v) (hsuv : s ⊆ u ∪ v) (hsv : (s ∩ v).Nonempty) (hs : IsPreconnected s) :
    s ⊆ v :=
  hs.subset_left_of_subset_union hv hu huv.symm (union_comm u v ▸ hsuv) hsv
Preconnected Subset Contained in Right Component of Open Partition
Informal description
Let $s$ be a preconnected subset of a topological space, and let $u$ and $v$ be two disjoint open sets such that $s \subseteq u \cup v$. If $s$ has a nonempty intersection with $v$, then $s$ is entirely contained in $v$.
IsPreconnected.subset_of_closure_inter_subset theorem
(hs : IsPreconnected s) (hu : IsOpen u) (h'u : (s ∩ u).Nonempty) (h : closure u ∩ s ⊆ u) : s ⊆ u
Full source 
/-- If a preconnected set `s` intersects an open set `u`, and limit points of `u` inside `s` are
contained in `u`, then the whole set `s` is contained in `u`. -/
theorem IsPreconnected.subset_of_closure_inter_subset (hs : IsPreconnected s) (hu : IsOpen u)
    (h'u : (s ∩ u).Nonempty) (h : closureclosure u ∩ sclosure u ∩ s ⊆ u) : s ⊆ u := by
  have A : s ⊆ u ∪ (closure u)ᶜ := by
    intro x hx
    by_cases xu : x ∈ u
    · exact Or.inl xu
    · right
      intro h'x
      exact xu (h (mem_inter h'x hx))
  apply hs.subset_left_of_subset_union hu isClosed_closure.isOpen_compl _ A h'u
  exact disjoint_compl_right.mono_right (compl_subset_compl.2 subset_closure)
Preconnected Subset Contained in Open Set via Closure Condition
Informal description
Let $s$ be a preconnected subset of a topological space $X$, and let $u$ be an open subset of $X$ such that: 1. $s \cap u$ is nonempty, and 2. The intersection of the closure of $u$ with $s$ is contained in $u$. Then $s$ is entirely contained in $u$.
IsPreconnected.prod theorem
[TopologicalSpace β] {s : Set α} {t : Set β} (hs : IsPreconnected s) (ht : IsPreconnected t) : IsPreconnected (s ×ˢ t)
Full source 
theorem IsPreconnected.prod [TopologicalSpace β] {s : Set α} {t : Set β} (hs : IsPreconnected s)
    (ht : IsPreconnected t) : IsPreconnected (s ×ˢ t) := by
  apply isPreconnected_of_forall_pair
  rintro ⟨a₁, b₁⟩ ⟨ha₁, hb₁⟩ ⟨a₂, b₂⟩ ⟨ha₂, hb₂⟩
  refine ⟨Prod.mk a₁ '' t ∪ flip Prod.mk b₂ '' s, ?_, .inl ⟨b₁, hb₁, rfl⟩, .inr ⟨a₂, ha₂, rfl⟩, ?_⟩
  · rintro _ (⟨y, hy, rfl⟩ | ⟨x, hx, rfl⟩)
    exacts [⟨ha₁, hy⟩, ⟨hx, hb₂⟩]
  · exact (ht.image _ (by fun_prop)).union (a₁, b₂) ⟨b₂, hb₂, rfl⟩
      ⟨a₁, ha₁, rfl⟩ (hs.image _ (Continuous.prodMk_left _).continuousOn)
Product of Preconnected Sets is Preconnected
Informal description
Let $\alpha$ and $\beta$ be topological spaces, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be preconnected subsets. Then the Cartesian product $s \times t$ is preconnected in the product space $\alpha \times \beta$.
IsConnected.prod theorem
[TopologicalSpace β] {s : Set α} {t : Set β} (hs : IsConnected s) (ht : IsConnected t) : IsConnected (s ×ˢ t)
Full source 
theorem IsConnected.prod [TopologicalSpace β] {s : Set α} {t : Set β} (hs : IsConnected s)
    (ht : IsConnected t) : IsConnected (s ×ˢ t) :=
  ⟨hs.1.prod ht.1, hs.2.prod ht.2⟩
Product of Connected Sets is Connected
Informal description
Let $X$ and $Y$ be topological spaces, and let $s \subseteq X$ and $t \subseteq Y$ be connected subsets. Then the Cartesian product $s \times t$ is connected in the product space $X \times Y$.
isPreconnected_univ_pi theorem
[∀ i, TopologicalSpace (π i)] {s : ∀ i, Set (π i)} (hs : ∀ i, IsPreconnected (s i)) : IsPreconnected (pi univ s)
Full source 
theorem isPreconnected_univ_pi [∀ i, TopologicalSpace (π i)] {s : ∀ i, Set (π i)}
    (hs : ∀ i, IsPreconnected (s i)) : IsPreconnected (pi univ s) := by
  rintro u v uo vo hsuv ⟨f, hfs, hfu⟩ ⟨g, hgs, hgv⟩
  classical
  rcases exists_finset_piecewise_mem_of_mem_nhds (uo.mem_nhds hfu) g with ⟨I, hI⟩
  induction I using Finset.induction_on with
  | empty =>
    refine ⟨g, hgs, ⟨?_, hgv⟩⟩
    simpa using hI
  | insert i I _ ihI =>
    rw [Finset.piecewise_insert] at hI
    have := I.piecewise_mem_set_pi hfs hgs
    refine (hsuv this).elim ihI fun h => ?_
    set S := update (I.piecewise f g) i '' s i
    have hsub : S ⊆ pi univ s := by
      refine image_subset_iff.2 fun z hz => ?_
      rwa [update_preimage_univ_pi]
      exact fun j _ => this j trivial
    have hconn : IsPreconnected S :=
      (hs i).image _ (continuous_const.update i continuous_id).continuousOn
    have hSu : (S ∩ u).Nonempty := ⟨_, mem_image_of_mem _ (hfs _ trivial), hI⟩
    have hSv : (S ∩ v).Nonempty := ⟨_, ⟨_, this _ trivial, update_eq_self _ _⟩, h⟩
    refine (hconn u v uo vo (hsub.trans hsuv) hSu hSv).mono ?_
    exact inter_subset_inter_left _ hsub
Preconnectedness of the Product of Preconnected Sets
Informal description
For a family of topological spaces $\{\pi_i\}_{i \in \iota}$ and a family of subsets $s_i \subseteq \pi_i$ where each $s_i$ is preconnected, the product set $\prod_{i \in \iota} s_i$ is preconnected in the product topology.
isConnected_univ_pi theorem
[∀ i, TopologicalSpace (π i)] {s : ∀ i, Set (π i)} : IsConnected (pi univ s) ↔ ∀ i, IsConnected (s i)
Full source 
@[simp]
theorem isConnected_univ_pi [∀ i, TopologicalSpace (π i)] {s : ∀ i, Set (π i)} :
    IsConnectedIsConnected (pi univ s) ↔ ∀ i, IsConnected (s i) := by
  simp only [IsConnected, ← univ_pi_nonempty_iff, forall_and, and_congr_right_iff]
  refine fun hne => ⟨fun hc i => ?_, isPreconnected_univ_pi⟩
  rw [← eval_image_univ_pi hne]
  exact hc.image _ (continuous_apply _).continuousOn
Connectedness of Product Space $\prod_{i} s_i$ is Equivalent to Connectedness of Each $s_i$
Informal description
For a family of topological spaces $\{\pi_i\}_{i \in \iota}$ and a family of subsets $s_i \subseteq \pi_i$, the product set $\prod_{i \in \iota} s_i$ is connected if and only if each $s_i$ is connected.
connectedComponent definition
(x : α) : Set α
Full source 
/-- The connected component of a point is the maximal connected set
that contains this point. -/
def connectedComponent (x : α) : Set α :=
  ⋃₀ { s : Set α | IsPreconnected s ∧ x ∈ s }
Connected component of a point in a topological space
Informal description
The connected component of a point $x$ in a topological space $\alpha$ is the union of all preconnected subsets of $\alpha$ that contain $x$. It is the largest connected set containing $x$.
connectedComponentIn definition
(F : Set α) (x : α) : Set α
Full source 
/-- Given a set `F` in a topological space `α` and a point `x : α`, the connected
component of `x` in `F` is the connected component of `x` in the subtype `F` seen as
a set in `α`. This definition does not make sense if `x` is not in `F` so we return the
empty set in this case. -/
def connectedComponentIn (F : Set α) (x : α) : Set α :=
  if h : x ∈ F then (↑) '' connectedComponent (⟨x, h⟩ : F) else ∅
Connected component of a point in a subset of a topological space
Informal description
Given a topological space $\alpha$, a subset $F \subseteq \alpha$, and a point $x \in \alpha$, the connected component of $x$ in $F$ is defined as follows: If $x$ belongs to $F$, then it is the image of the connected component of $\langle x, h \rangle$ in the subspace topology of $F$ (where $h$ is the proof that $x \in F$). If $x$ does not belong to $F$, the connected component is defined to be the empty set.
connectedComponentIn_eq_image theorem
{F : Set α} {x : α} (h : x ∈ F) : connectedComponentIn F x = (↑) '' connectedComponent (⟨x, h⟩ : F)
Full source 
theorem connectedComponentIn_eq_image {F : Set α} {x : α} (h : x ∈ F) :
    connectedComponentIn F x = (↑) '' connectedComponent (⟨x, h⟩ : F) :=
  dif_pos h
Connected Component in Subset Equals Image of Subspace Connected Component
Informal description
For a subset $F$ of a topological space $\alpha$ and a point $x \in F$, the connected component of $x$ in $F$ is equal to the image of the connected component of $\langle x, h \rangle$ in the subspace topology of $F$ under the inclusion map, where $h$ is the proof that $x \in F$.
connectedComponentIn_eq_empty theorem
{F : Set α} {x : α} (h : x ∉ F) : connectedComponentIn F x = ∅
Full source 
theorem connectedComponentIn_eq_empty {F : Set α} {x : α} (h : x ∉ F) :
    connectedComponentIn F x = ∅ :=
  dif_neg h
Empty Connected Component for Points Outside Subset
Informal description
For any subset $F$ of a topological space $\alpha$ and any point $x \in \alpha$ not belonging to $F$, the connected component of $x$ in $F$ is the empty set, i.e., $\text{connectedComponentIn}(F, x) = \emptyset$.
mem_connectedComponentIn theorem
{x : α} {F : Set α} (hx : x ∈ F) : x ∈ connectedComponentIn F x
Full source 
theorem mem_connectedComponentIn {x : α} {F : Set α} (hx : x ∈ F) :
    x ∈ connectedComponentIn F x := by
  simp [connectedComponentIn_eq_image hx, mem_connectedComponent, hx]
Point Belongs to Its Connected Component in a Subset
Informal description
For any point $x$ in a topological space $\alpha$ and any subset $F \subseteq \alpha$, if $x \in F$, then $x$ belongs to the connected component of $x$ in $F$.
connectedComponentIn_nonempty_iff theorem
{x : α} {F : Set α} : (connectedComponentIn F x).Nonempty ↔ x ∈ F
Full source 
theorem connectedComponentIn_nonempty_iff {x : α} {F : Set α} :
    (connectedComponentIn F x).Nonempty ↔ x ∈ F := by
  rw [connectedComponentIn]
  split_ifs <;> simp [connectedComponent_nonempty, *]
Nonemptiness of Connected Component in Subset iff Point Belongs to Subset
Informal description
For any point $x$ in a topological space $\alpha$ and any subset $F \subseteq \alpha$, the connected component of $x$ in $F$ is nonempty if and only if $x$ belongs to $F$.
isPreconnected_connectedComponent theorem
{x : α} : IsPreconnected (connectedComponent x)
Full source 
theorem isPreconnected_connectedComponent {x : α} : IsPreconnected (connectedComponent x) :=
  isPreconnected_sUnion x _ (fun _ => And.right) fun _ => And.left
Connected Components are Preconnected
Informal description
For any point $x$ in a topological space $\alpha$, the connected component of $x$ is a preconnected subset of $\alpha$. That is, there is no nontrivial open partition of the connected component of $x$.
isPreconnected_connectedComponentIn theorem
{x : α} {F : Set α} : IsPreconnected (connectedComponentIn F x)
Full source 
theorem isPreconnected_connectedComponentIn {x : α} {F : Set α} :
    IsPreconnected (connectedComponentIn F x) := by
  rw [connectedComponentIn]; split_ifs
  · exact IsInducing.subtypeVal.isPreconnected_image.mpr isPreconnected_connectedComponent
  · exact isPreconnected_empty
Preconnectedness of Connected Components in Subsets
Informal description
For any point $x$ in a topological space $\alpha$ and any subset $F \subseteq \alpha$, the connected component of $x$ in $F$ is a preconnected subset of $\alpha$. That is, there is no nontrivial open partition of the connected component of $x$ in $F$.
isConnected_connectedComponentIn_iff theorem
{x : α} {F : Set α} : IsConnected (connectedComponentIn F x) ↔ x ∈ F
Full source 
theorem isConnected_connectedComponentIn_iff {x : α} {F : Set α} :
    IsConnectedIsConnected (connectedComponentIn F x) ↔ x ∈ F := by
  simp_rw [← connectedComponentIn_nonempty_iff, IsConnected, isPreconnected_connectedComponentIn,
    and_true]
Characterization of Connectedness for Connected Components in Subsets
Informal description
For a topological space $\alpha$, a subset $F \subseteq \alpha$, and a point $x \in \alpha$, the connected component of $x$ in $F$ is connected if and only if $x$ belongs to $F$.
IsPreconnected.subset_connectedComponent theorem
{x : α} {s : Set α} (H1 : IsPreconnected s) (H2 : x ∈ s) : s ⊆ connectedComponent x
Full source 
theorem IsPreconnected.subset_connectedComponent {x : α} {s : Set α} (H1 : IsPreconnected s)
    (H2 : x ∈ s) : s ⊆ connectedComponent x := fun _z hz => mem_sUnion_of_mem hz ⟨H1, H2⟩
Preconnected subsets are contained in their connected components
Informal description
Let $s$ be a preconnected subset of a topological space $\alpha$, and let $x$ be an element of $s$. Then $s$ is contained in the connected component of $x$, i.e., $s \subseteq \text{connectedComponent}(x)$.
IsPreconnected.subset_connectedComponentIn theorem
{x : α} {F : Set α} (hs : IsPreconnected s) (hxs : x ∈ s) (hsF : s ⊆ F) : s ⊆ connectedComponentIn F x
Full source 
theorem IsPreconnected.subset_connectedComponentIn {x : α} {F : Set α} (hs : IsPreconnected s)
    (hxs : x ∈ s) (hsF : s ⊆ F) : s ⊆ connectedComponentIn F x := by
  have : IsPreconnected (((↑) : F → α) ⁻¹' s) := by
    refine IsInducing.subtypeVal.isPreconnected_image.mp ?_
    rwa [Subtype.image_preimage_coe, inter_eq_right.mpr hsF]
  have h2xs : (⟨x, hsF hxs⟩ : F) ∈ (↑) ⁻¹' s := by
    rw [mem_preimage]
    exact hxs
  have := this.subset_connectedComponent h2xs
  rw [connectedComponentIn_eq_image (hsF hxs)]
  refine Subset.trans ?_ (image_subset _ this)
  rw [Subtype.image_preimage_coe, inter_eq_right.mpr hsF]
Preconnected subsets are contained in their connected components within a larger set
Informal description
Let $s$ be a preconnected subset of a topological space $\alpha$, and let $x \in s$ be a point. If $s$ is contained in a subset $F \subseteq \alpha$, then $s$ is contained in the connected component of $x$ within $F$, i.e., $s \subseteq \text{connectedComponentIn}(F, x)$.
IsConnected.subset_connectedComponent theorem
{x : α} {s : Set α} (H1 : IsConnected s) (H2 : x ∈ s) : s ⊆ connectedComponent x
Full source 
theorem IsConnected.subset_connectedComponent {x : α} {s : Set α} (H1 : IsConnected s)
    (H2 : x ∈ s) : s ⊆ connectedComponent x :=
  H1.2.subset_connectedComponent H2
Connected subsets are contained in their connected components
Informal description
For any connected subset $s$ of a topological space $\alpha$ and any point $x \in s$, the set $s$ is contained in the connected component of $x$, i.e., $s \subseteq \text{connectedComponent}(x)$.
IsPreconnected.connectedComponentIn theorem
{x : α} {F : Set α} (h : IsPreconnected F) (hx : x ∈ F) : connectedComponentIn F x = F
Full source 
theorem IsPreconnected.connectedComponentIn {x : α} {F : Set α} (h : IsPreconnected F)
    (hx : x ∈ F) : connectedComponentIn F x = F :=
  (connectedComponentIn_subset F x).antisymm (h.subset_connectedComponentIn hx subset_rfl)
Connected Component of a Point in a Preconnected Set Equals the Set
Informal description
Let $F$ be a preconnected subset of a topological space $\alpha$ and let $x \in F$ be a point. Then the connected component of $x$ in $F$ equals $F$ itself, i.e., $\text{connectedComponentIn}(F, x) = F$.
connectedComponent_eq theorem
{x y : α} (h : y ∈ connectedComponent x) : connectedComponent x = connectedComponent y
Full source 
theorem connectedComponent_eq {x y : α} (h : y ∈ connectedComponent x) :
    connectedComponent x = connectedComponent y :=
  eq_of_subset_of_subset (isConnected_connectedComponent.subset_connectedComponent h)
    (isConnected_connectedComponent.subset_connectedComponent
      (Set.mem_of_mem_of_subset mem_connectedComponent
        (isConnected_connectedComponent.subset_connectedComponent h)))
Connected Components Equality for Points in the Same Component
Informal description
For any two points $x$ and $y$ in a topological space $\alpha$, if $y$ belongs to the connected component of $x$, then the connected component of $x$ equals the connected component of $y$.
connectedComponent_eq_iff_mem theorem
{x y : α} : connectedComponent x = connectedComponent y ↔ x ∈ connectedComponent y
Full source 
theorem connectedComponent_eq_iff_mem {x y : α} :
    connectedComponentconnectedComponent x = connectedComponent y ↔ x ∈ connectedComponent y :=
  ⟨fun h => h ▸ mem_connectedComponent, fun h => (connectedComponent_eq h).symm⟩
Equality of Connected Components via Membership
Informal description
For any two points $x$ and $y$ in a topological space $\alpha$, the connected component of $x$ equals the connected component of $y$ if and only if $x$ belongs to the connected component of $y$.
connectedComponentIn_eq theorem
{x y : α} {F : Set α} (h : y ∈ connectedComponentIn F x) : connectedComponentIn F x = connectedComponentIn F y
Full source 
theorem connectedComponentIn_eq {x y : α} {F : Set α} (h : y ∈ connectedComponentIn F x) :
    connectedComponentIn F x = connectedComponentIn F y := by
  have hx : x ∈ F := connectedComponentIn_nonempty_iff.mp ⟨y, h⟩
  simp_rw [connectedComponentIn_eq_image hx] at h ⊢
  obtain ⟨⟨y, hy⟩, h2y, rfl⟩ := h
  simp_rw [connectedComponentIn_eq_image hy, connectedComponent_eq h2y]
Equality of Connected Components in Subset for Points in the Same Component
Informal description
For any two points $x$ and $y$ in a topological space $\alpha$ and any subset $F \subseteq \alpha$, if $y$ belongs to the connected component of $x$ in $F$, then the connected component of $x$ in $F$ equals the connected component of $y$ in $F$.
connectedComponentIn_univ theorem
(x : α) : connectedComponentIn univ x = connectedComponent x
Full source 
theorem connectedComponentIn_univ (x : α) : connectedComponentIn univ x = connectedComponent x :=
  subset_antisymm
    (isPreconnected_connectedComponentIn.subset_connectedComponent <|
      mem_connectedComponentIn trivial)
    (isPreconnected_connectedComponent.subset_connectedComponentIn mem_connectedComponent <|
      subset_univ _)
Connected Component in Universal Set Equals Connected Component in Space
Informal description
For any point $x$ in a topological space $\alpha$, the connected component of $x$ in the universal set $\text{univ}$ (the entire space) equals the connected component of $x$ in $\alpha$.
connectedComponent_disjoint theorem
{x y : α} (h : connectedComponent x ≠ connectedComponent y) : Disjoint (connectedComponent x) (connectedComponent y)
Full source 
theorem connectedComponent_disjoint {x y : α} (h : connectedComponentconnectedComponent x ≠ connectedComponent y) :
    Disjoint (connectedComponent x) (connectedComponent y) :=
  Set.disjoint_left.2 fun _ h1 h2 =>
    h ((connectedComponent_eq h1).trans (connectedComponent_eq h2).symm)
Disjointness of Distinct Connected Components
Informal description
For any two points $x$ and $y$ in a topological space $\alpha$, if the connected component of $x$ is not equal to the connected component of $y$, then the connected components of $x$ and $y$ are disjoint sets.
Continuous.image_connectedComponent_subset theorem
[TopologicalSpace β] {f : α → β} (h : Continuous f) (a : α) : f '' connectedComponent a ⊆ connectedComponent (f a)
Full source 
theorem Continuous.image_connectedComponent_subset [TopologicalSpace β] {f : α → β}
    (h : Continuous f) (a : α) : f '' connectedComponent af '' connectedComponent a ⊆ connectedComponent (f a) :=
  (isConnected_connectedComponent.image f h.continuousOn).subset_connectedComponent
    ((mem_image f (connectedComponent a) (f a)).2 ⟨a, mem_connectedComponent, rfl⟩)
Continuous Maps Preserve Connected Components: $f(\text{connectedComponent}(a)) \subseteq \text{connectedComponent}(f(a))$
Informal description
Let $X$ and $Y$ be topological spaces, and let $f \colon X \to Y$ be a continuous function. For any point $a \in X$, the image of the connected component of $a$ under $f$ is contained in the connected component of $f(a)$ in $Y$. In other words, $f(\text{connectedComponent}(a)) \subseteq \text{connectedComponent}(f(a))$.
Continuous.image_connectedComponentIn_subset theorem
[TopologicalSpace β] {f : α → β} {s : Set α} {a : α} (hf : Continuous f) (hx : a ∈ s) : f '' connectedComponentIn s a ⊆ connectedComponentIn (f '' s) (f a)
Full source 
theorem Continuous.image_connectedComponentIn_subset [TopologicalSpace β] {f : α → β} {s : Set α}
    {a : α} (hf : Continuous f) (hx : a ∈ s) :
    f '' connectedComponentIn s af '' connectedComponentIn s a ⊆ connectedComponentIn (f '' s) (f a) :=
  (isPreconnected_connectedComponentIn.image _ hf.continuousOn).subset_connectedComponentIn
    (mem_image_of_mem _ <| mem_connectedComponentIn hx)
    (image_subset _ <| connectedComponentIn_subset _ _)
Continuous Images Preserve Connected Components in Subsets: $f(\text{connectedComponentIn}(s, a)) \subseteq \text{connectedComponentIn}(f(s), f(a))$
Informal description
Let $X$ and $Y$ be topological spaces, $f \colon X \to Y$ a continuous function, $s \subseteq X$ a subset, and $a \in s$ a point. Then the image under $f$ of the connected component of $a$ in $s$ is contained in the connected component of $f(a)$ in $f(s)$. In other words: $$ f(\text{connectedComponentIn}(s, a)) \subseteq \text{connectedComponentIn}(f(s), f(a)) $$
Continuous.mapsTo_connectedComponent theorem
[TopologicalSpace β] {f : α → β} (h : Continuous f) (a : α) : MapsTo f (connectedComponent a) (connectedComponent (f a))
Full source 
theorem Continuous.mapsTo_connectedComponent [TopologicalSpace β] {f : α → β} (h : Continuous f)
    (a : α) : MapsTo f (connectedComponent a) (connectedComponent (f a)) :=
  mapsTo'.2 <| h.image_connectedComponent_subset a
Continuous Functions Preserve Connected Components: $f(\text{connectedComponent}(a)) \subseteq \text{connectedComponent}(f(a))$
Informal description
Let $X$ and $Y$ be topological spaces, and let $f \colon X \to Y$ be a continuous function. For any point $a \in X$, the function $f$ maps the connected component of $a$ into the connected component of $f(a)$. In other words, for every $x$ in the connected component of $a$, the image $f(x)$ belongs to the connected component of $f(a)$.
Continuous.mapsTo_connectedComponentIn theorem
[TopologicalSpace β] {f : α → β} {s : Set α} (h : Continuous f) {a : α} (hx : a ∈ s) : MapsTo f (connectedComponentIn s a) (connectedComponentIn (f '' s) (f a))
Full source 
theorem Continuous.mapsTo_connectedComponentIn [TopologicalSpace β] {f : α → β} {s : Set α}
    (h : Continuous f) {a : α} (hx : a ∈ s) :
    MapsTo f (connectedComponentIn s a) (connectedComponentIn (f '' s) (f a)) :=
  mapsTo'.2 <| image_connectedComponentIn_subset h hx
Continuous Functions Preserve Connected Components in Subsets: $f(\text{connectedComponentIn}(s, a)) \subseteq \text{connectedComponentIn}(f(s), f(a))$
Informal description
Let $X$ and $Y$ be topological spaces, $f \colon X \to Y$ a continuous function, $s \subseteq X$ a subset, and $a \in s$ a point. Then $f$ maps the connected component of $a$ in $s$ into the connected component of $f(a)$ in $f(s)$. In other words: $$ f(\text{connectedComponentIn}(s, a)) \subseteq \text{connectedComponentIn}(f(s), f(a)) $$
irreducibleComponent_subset_connectedComponent theorem
{x : α} : irreducibleComponent x ⊆ connectedComponent x
Full source 
theorem irreducibleComponent_subset_connectedComponent {x : α} :
    irreducibleComponentirreducibleComponent x ⊆ connectedComponent x :=
  isIrreducible_irreducibleComponent.isConnected.subset_connectedComponent mem_irreducibleComponent
Irreducible Component is Subset of Connected Component
Informal description
For any point $x$ in a topological space $\alpha$, the irreducible component of $x$ is contained in the connected component of $x$, i.e., $\text{irreducibleComponent}(x) \subseteq \text{connectedComponent}(x)$.
connectedComponentIn_mono theorem
(x : α) {F G : Set α} (h : F ⊆ G) : connectedComponentIn F x ⊆ connectedComponentIn G x
Full source 
@[mono]
theorem connectedComponentIn_mono (x : α) {F G : Set α} (h : F ⊆ G) :
    connectedComponentInconnectedComponentIn F x ⊆ connectedComponentIn G x := by
  by_cases hx : x ∈ F
  · rw [connectedComponentIn_eq_image hx, connectedComponentIn_eq_image (h hx), ←
      show ((↑) : G → α) ∘ inclusion h = (↑) from rfl, image_comp]
    exact image_subset _ ((continuous_inclusion h).image_connectedComponent_subset ⟨x, hx⟩)
  · rw [connectedComponentIn_eq_empty hx]
    exact Set.empty_subset _
Monotonicity of Connected Components with Respect to Subset Inclusion
Informal description
For any topological space $\alpha$, a point $x \in \alpha$, and subsets $F, G \subseteq \alpha$ with $F \subseteq G$, the connected component of $x$ in $F$ is contained in the connected component of $x$ in $G$, i.e., $$\text{connectedComponentIn}(F, x) \subseteq \text{connectedComponentIn}(G, x).$$
PreconnectedSpace structure
(α : Type u) [TopologicalSpace α]
Full source 
/-- A preconnected space is one where there is no non-trivial open partition. -/
class PreconnectedSpace (α : Type u) [TopologicalSpace α] : Prop where
  /-- The universal set `Set.univ` in a preconnected space is a preconnected set. -/
  isPreconnected_univ : IsPreconnected (univ : Set α)
Preconnected topological space
Informal description
A topological space $\alpha$ is called *preconnected* if it cannot be partitioned into two nonempty disjoint open subsets. In other words, there are no two nonempty open sets $U$ and $V$ such that $U \cup V = \alpha$ and $U \cap V = \emptyset$.
ConnectedSpace structure
(α : Type u) [TopologicalSpace α] : Prop extends PreconnectedSpace α
Full source 
/-- A connected space is a nonempty one where there is no non-trivial open partition. -/
class ConnectedSpace (α : Type u) [TopologicalSpace α] : Prop extends PreconnectedSpace α where
  /-- A connected space is nonempty. -/
  toNonempty : Nonempty α
Connected topological space
Informal description
A topological space $\alpha$ is called *connected* if it is nonempty and cannot be partitioned into two nonempty disjoint open subsets. In other words, there are no two nonempty open sets $U$ and $V$ such that $U \cup V = \alpha$ and $U \cap V = \emptyset$.
connectedSpace_iff_univ theorem
: ConnectedSpace α ↔ IsConnected (univ : Set α)
Full source 
lemma connectedSpace_iff_univ : ConnectedSpaceConnectedSpace α ↔ IsConnected (univ : Set α) :=
  ⟨fun h ↦ ⟨univ_nonempty, h.1.1⟩,
   fun h ↦ ConnectedSpace.mk (toPreconnectedSpace := ⟨h.2⟩) ⟨h.1.some⟩⟩
Characterization of Connected Spaces via Universal Set
Informal description
A topological space $\alpha$ is connected if and only if the universal set $\text{univ} \subseteq \alpha$ is a connected subset.
isPreconnected_range theorem
[TopologicalSpace β] [PreconnectedSpace α] {f : α → β} (h : Continuous f) : IsPreconnected (range f)
Full source 
theorem isPreconnected_range [TopologicalSpace β] [PreconnectedSpace α] {f : α → β}
    (h : Continuous f) : IsPreconnected (range f) :=
  @image_univ _ _ f ▸ isPreconnected_univ.image _ h.continuousOn
Continuous Image of a Preconnected Space is Preconnected
Informal description
Let $\alpha$ and $\beta$ be topological spaces, with $\alpha$ preconnected. If $f \colon \alpha \to \beta$ is a continuous function, then the range of $f$ is a preconnected subset of $\beta$.
isConnected_range theorem
[TopologicalSpace β] [ConnectedSpace α] {f : α → β} (h : Continuous f) : IsConnected (range f)
Full source 
theorem isConnected_range [TopologicalSpace β] [ConnectedSpace α] {f : α → β} (h : Continuous f) :
    IsConnected (range f) :=
  ⟨range_nonempty f, isPreconnected_range h⟩
Continuous Image of a Connected Space is Connected
Informal description
Let $\alpha$ and $\beta$ be topological spaces, with $\alpha$ connected. If $f \colon \alpha \to \beta$ is a continuous function, then the range of $f$ is a connected subset of $\beta$.
Function.Surjective.connectedSpace theorem
[ConnectedSpace α] [TopologicalSpace β] {f : α → β} (hf : Surjective f) (hf' : Continuous f) : ConnectedSpace β
Full source 
theorem Function.Surjective.connectedSpace [ConnectedSpace α] [TopologicalSpace β]
    {f : α → β} (hf : Surjective f) (hf' : Continuous f) : ConnectedSpace β := by
  rw [connectedSpace_iff_univ, ← hf.range_eq]
  exact isConnected_range hf'
Continuous Surjective Image of a Connected Space is Connected
Informal description
Let $\alpha$ and $\beta$ be topological spaces, with $\alpha$ connected. If $f \colon \alpha \to \beta$ is a continuous surjective function, then $\beta$ is also connected.
DenseRange.preconnectedSpace theorem
[TopologicalSpace β] [PreconnectedSpace α] {f : α → β} (hf : DenseRange f) (hc : Continuous f) : PreconnectedSpace β
Full source 
theorem DenseRange.preconnectedSpace [TopologicalSpace β] [PreconnectedSpace α] {f : α → β}
    (hf : DenseRange f) (hc : Continuous f) : PreconnectedSpace β :=
  ⟨hf.closure_eq ▸ (isPreconnected_range hc).closure⟩
Continuous Dense Image of a Preconnected Space is Preconnected
Informal description
Let $\alpha$ and $\beta$ be topological spaces, with $\alpha$ preconnected. If $f \colon \alpha \to \beta$ is a continuous function with dense range, then $\beta$ is a preconnected space.
connectedSpace_iff_connectedComponent theorem
: ConnectedSpace α ↔ ∃ x : α, connectedComponent x = univ
Full source 
theorem connectedSpace_iff_connectedComponent :
    ConnectedSpaceConnectedSpace α ↔ ∃ x : α, connectedComponent x = univ := by
  constructor
  · rintro ⟨⟨x⟩⟩
    exact
      ⟨x, eq_univ_of_univ_subset <| isPreconnected_univ.subset_connectedComponent (mem_univ x)⟩
  · rintro ⟨x, h⟩
    haveI : PreconnectedSpace α :=
      ⟨by rw [← h]; exact isPreconnected_connectedComponent⟩
    exact ⟨⟨x⟩⟩
Characterization of Connected Spaces via Connected Components
Informal description
A topological space $\alpha$ is connected if and only if there exists a point $x \in \alpha$ such that the connected component of $x$ is the entire space, i.e., $\text{connectedComponent}(x) = \text{univ}$.
preconnectedSpace_iff_connectedComponent theorem
: PreconnectedSpace α ↔ ∀ x : α, connectedComponent x = univ
Full source 
theorem preconnectedSpace_iff_connectedComponent :
    PreconnectedSpacePreconnectedSpace α ↔ ∀ x : α, connectedComponent x = univ := by
  constructor
  · intro h x
    exact eq_univ_of_univ_subset <| isPreconnected_univ.subset_connectedComponent (mem_univ x)
  · intro h
    rcases isEmpty_or_nonempty α with hα | hα
    · exact ⟨by rw [univ_eq_empty_iff.mpr hα]; exact isPreconnected_empty⟩
    · exact ⟨by rw [← h (Classical.choice hα)]; exact isPreconnected_connectedComponent⟩
Characterization of Preconnected Spaces via Connected Components
Informal description
A topological space $\alpha$ is preconnected if and only if for every point $x \in \alpha$, the connected component of $x$ is equal to the entire space $\alpha$.
PreconnectedSpace.connectedComponent_eq_univ theorem
{X : Type*} [TopologicalSpace X] [h : PreconnectedSpace X] (x : X) : connectedComponent x = univ
Full source 
@[simp]
theorem PreconnectedSpace.connectedComponent_eq_univ {X : Type*} [TopologicalSpace X]
    [h : PreconnectedSpace X] (x : X) : connectedComponent x = univ :=
  preconnectedSpace_iff_connectedComponent.mp h x
Connected Components in Preconnected Spaces Cover the Whole Space
Informal description
For a preconnected topological space $X$ and any point $x \in X$, the connected component of $x$ is equal to the entire space $X$, i.e., $\text{connectedComponent}(x) = X$.
instPreconnectedSpaceProd instance
[TopologicalSpace β] [PreconnectedSpace α] [PreconnectedSpace β] : PreconnectedSpace (α × β)
Full source 
instance [TopologicalSpace β] [PreconnectedSpace α] [PreconnectedSpace β] :
    PreconnectedSpace (α × β) :=
  ⟨by
    rw [← univ_prod_univ]
    exact isPreconnected_univ.prod isPreconnected_univ⟩
Product of Preconnected Spaces is Preconnected
Informal description
For any topological spaces $\alpha$ and $\beta$, if both $\alpha$ and $\beta$ are preconnected, then their product space $\alpha \times \beta$ is also preconnected.
instConnectedSpaceProd instance
[TopologicalSpace β] [ConnectedSpace α] [ConnectedSpace β] : ConnectedSpace (α × β)
Full source 
instance [TopologicalSpace β] [ConnectedSpace α] [ConnectedSpace β] : ConnectedSpace (α × β) :=
  ⟨inferInstance⟩
Product of Connected Spaces is Connected
Informal description
For any topological spaces $\alpha$ and $\beta$, if both $\alpha$ and $\beta$ are connected, then their product space $\alpha \times \beta$ is also connected.
instPreconnectedSpaceForall instance
[∀ i, TopologicalSpace (π i)] [∀ i, PreconnectedSpace (π i)] : PreconnectedSpace (∀ i, π i)
Full source 
instance [∀ i, TopologicalSpace (π i)] [∀ i, PreconnectedSpace (π i)] :
    PreconnectedSpace (∀ i, π i) :=
  ⟨by rw [← pi_univ univ]; exact isPreconnected_univ_pi fun i => isPreconnected_univ⟩
Product of Preconnected Spaces is Preconnected
Informal description
For any family of topological spaces $\{\pi_i\}_{i \in \iota}$ where each $\pi_i$ is preconnected, the product space $\prod_{i \in \iota} \pi_i$ is also preconnected.
instConnectedSpaceForall instance
[∀ i, TopologicalSpace (π i)] [∀ i, ConnectedSpace (π i)] : ConnectedSpace (∀ i, π i)
Full source 
instance [∀ i, TopologicalSpace (π i)] [∀ i, ConnectedSpace (π i)] : ConnectedSpace (∀ i, π i) :=
  ⟨inferInstance⟩
Product of Connected Spaces is Connected
Informal description
For any family of topological spaces $\{\pi_i\}_{i \in \iota}$ where each $\pi_i$ is connected, the product space $\prod_{i \in \iota} \pi_i$ is also connected.
Subtype.preconnectedSpace theorem
{s : Set α} (h : IsPreconnected s) : PreconnectedSpace s
Full source 
theorem Subtype.preconnectedSpace {s : Set α} (h : IsPreconnected s) : PreconnectedSpace s where
  isPreconnected_univ := by
    rwa [← IsInducing.subtypeVal.isPreconnected_image, image_univ, Subtype.range_val]
Preconnected Subset Induces Preconnected Subspace
Informal description
For any subset $s$ of a topological space $\alpha$, if $s$ is preconnected (i.e., it cannot be partitioned into two nonempty disjoint open subsets relative to $s$), then the subspace topology on $s$ makes it a preconnected space.
Subtype.connectedSpace theorem
{s : Set α} (h : IsConnected s) : ConnectedSpace s
Full source 
theorem Subtype.connectedSpace {s : Set α} (h : IsConnected s) : ConnectedSpace s where
  toPreconnectedSpace := Subtype.preconnectedSpace h.isPreconnected
  toNonempty := h.nonempty.to_subtype
Connected Subset Induces Connected Subspace
Informal description
For any subset $s$ of a topological space $\alpha$, if $s$ is connected (i.e., nonempty and has no nontrivial open partition), then the subspace topology on $s$ makes it a connected space.
isPreconnected_iff_preconnectedSpace theorem
{s : Set α} : IsPreconnected s ↔ PreconnectedSpace s
Full source 
theorem isPreconnected_iff_preconnectedSpace {s : Set α} : IsPreconnectedIsPreconnected s ↔ PreconnectedSpace s :=
  ⟨Subtype.preconnectedSpace, fun h => by
    simpa using isPreconnected_univ.image ((↑) : s → α) continuous_subtype_val.continuousOn⟩
Preconnected Subset Characterization via Subspace Preconnectedness
Informal description
A subset $s$ of a topological space $\alpha$ is preconnected if and only if the subspace $s$ with the induced topology is a preconnected space.
isConnected_iff_connectedSpace theorem
{s : Set α} : IsConnected s ↔ ConnectedSpace s
Full source 
theorem isConnected_iff_connectedSpace {s : Set α} : IsConnectedIsConnected s ↔ ConnectedSpace s :=
  ⟨Subtype.connectedSpace, fun h =>
    ⟨nonempty_subtype.mp h.2, isPreconnected_iff_preconnectedSpace.mpr h.1⟩⟩
Characterization of Connected Subsets via Subspace Connectedness
Informal description
A subset $s$ of a topological space $\alpha$ is connected if and only if the subspace $s$ with the induced topology is a connected space (i.e., nonempty and cannot be partitioned into two nonempty disjoint open subsets).