isPreconnected_of_forall_constant
theorem isPreconnected_of_forall_constant :
∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
(∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y) → IsPreconnected s
This theorem states that for any set `s` in a topological space `α`, if every map to `Bool` (a discrete two-element space) that is continuous on `s` is constant on `s` (meaning that the output of the map is the same for any two points `x` and `y` in `s`), then `s` is preconnected. In other words, if there is no continuous map from `s` to the 2-element set (Bool) that can distinguish between different points in `s`, implying that there is no 'boundary' or 'gaps' in `s`, then `s` is preconnected, implying that it cannot be represented as the union of two nonempty disjoint open sets.
More concisely: A subset of a topological space is preconnected if and only if no continuous function from it to the two-element Boolean algebra distinguishes between distinct points.
|
IsPreconnected.subset_of_closure_inter_subset
theorem IsPreconnected.subset_of_closure_inter_subset :
∀ {α : Type u} [inst : TopologicalSpace α] {s u : Set α},
IsPreconnected s → IsOpen u → (s ∩ u).Nonempty → closure u ∩ s ⊆ u → s ⊆ u
The theorem `IsPreconnected.subset_of_closure_inter_subset` states that for any type `α` equipped with a topology (indicated by `TopologicalSpace α`), and any two sets `s` and `u` of this type, if `s` is a preconnected set and `u` is an open set such that `s` and `u` have a nonempty intersection, and all limit points of `u` that lie inside `s` are actually contained in `u`, then it follows that the entire set `s` is a subset of `u`.
In other words, under these conditions, a preconnected set `s` that intersects with an open set `u` and whose intersection with the closure of `u` is a subset of `u`, must be entirely contained within `u`. This theorem is a statement about the interplay between preconnected sets, open sets, and limit points in a topological space.
More concisely: If `s` is a preconnected set, `u` is an open set, and `s ∩ u` is nonempty with `s ∩ cl(u) ⊆ u`, then `s ⊆ u`, where `α` is a topological space.
|
Subtype.preconnectedSpace
theorem Subtype.preconnectedSpace :
∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsPreconnected s → PreconnectedSpace ↑s
The `Subtype.preconnectedSpace` theorem states that for any type `α` equipped with a topology (i.e., a `TopologicalSpace α`), and any set `s` of this type, if the set `s` is preconnected (as per the definition of `IsPreconnected`), then the corresponding subtype `↑s` is a preconnected space in the sense of the mathematical definition of preconnected spaces. Here, `↑s` refers to the subset of the topological space `α` that corresponds to the set `s`. In other words, this theorem links the property of being preconnected for a set in a given topological space to the property of being a preconnected space when we consider that set as a subspace of the original topological space.
More concisely: If `α` is a topological space and `s ⊆ α` is preconnected, then the subspace `↑s` is a preconnected space.
|
mem_connectedComponentIn
theorem mem_connectedComponentIn :
∀ {α : Type u} [inst : TopologicalSpace α] {x : α} {F : Set α}, x ∈ F → x ∈ connectedComponentIn F x
This theorem states that for any type `α` equipped with a topological structure, a set `F` in `α`, and a point `x` in `α`, if `x` belongs to the set `F`, then `x` is an element of its connected component in `F`. In other words, given a topological space and a point in a set of that space, the point is part of the subset that forms the connected component it belongs to in the original set.
More concisely: In a topological space, any point in a connected subset belongs to its connected component.
|
isPreconnected_of_forall_pair
theorem isPreconnected_of_forall_pair :
∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
(∀ x ∈ s, ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t) → IsPreconnected s
The theorem `isPreconnected_of_forall_pair` states that for any set `s` in a topological space `α`, if for every pair of points in `s` there exists a preconnected subset `t` of `s` that contains both points, then `s` itself is preconnected. In other words, a set is preconnected if any two points in the set can be connected within the set via preconnected subsets.
More concisely: If every pair of points in a set has a preconnected subset containing them, then the set itself is preconnected.
|
IsConnected.subset_connectedComponent
theorem IsConnected.subset_connectedComponent :
∀ {α : Type u} [inst : TopologicalSpace α] {x : α} {s : Set α}, IsConnected s → x ∈ s → s ⊆ connectedComponent x
The theorem `IsConnected.subset_connectedComponent` states that for any type `α` with a topology, and for any set `s` of type `α` and an element `x` of type `α`, if `s` is a connected set and `x` is an element of `s`, then `s` is a subset of the connected component of `x`. In other words, every connected set that contains a given point is contained within the maximal connected set (the connected component) that contains the same point.
More concisely: For any topological space (α, T), connected set s ⊆ α, and x ∈ s, the subset s is included in the connected component of x.
|
IsPreconnected.subset_connectedComponent
theorem IsPreconnected.subset_connectedComponent :
∀ {α : Type u} [inst : TopologicalSpace α] {x : α} {s : Set α},
IsPreconnected s → x ∈ s → s ⊆ connectedComponent x
This theorem states that for any topological space `α` and for any point `x` and set `s` within `α`, if `s` is preconnected and `x` belongs to `s`, then `s` is a subset of the connected component of `x`. Here, a set is preconnected if there is no non-trivial open partition of it, and the connected component of a point is the largest preconnected set that contains the point.
More concisely: If a set `s` in a topological space `α` is preconnected and contains a point `x`, then `s` is a subset of the connected component of `x`.
|
mem_connectedComponent
theorem mem_connectedComponent : ∀ {α : Type u} [inst : TopologicalSpace α] {x : α}, x ∈ connectedComponent x := by
sorry
This theorem states that for any type `α` that has a topological space structure and any element `x` of the type `α`, `x` is an element of its own connected component. In other words, every point in a topological space is contained within its connected component. A connected component of a point in a topological space is the largest connected set that includes that point.
More concisely: Every point in a topological space is contained in its connected component.
|
disjoint_or_subset_of_isClopen
theorem disjoint_or_subset_of_isClopen :
∀ {α : Type u} [inst : TopologicalSpace α] {s t : Set α}, IsPreconnected s → IsClopen t → Disjoint s t ∨ s ⊆ t := by
sorry
The theorem states that for any type `α` that has a topological space structure, given any two sets `s` and `t` of type `α`, if `s` is preconnected and `t` is clopen, then `s` and `t` are either disjoint or `s` is a subset of `t`. In other words, a preconnected set is either entirely contained in a clopen set or does not share any elements with it. In the context of topology, a set is preconnected if there is no non-trivial open partition of the set, and a set is clopen if it is both open and closed. Two elements are considered disjoint if their greatest lower bound is the bottom element.
More concisely: If `α` is a type with a topological space structure, then for any preconnected sets `s` and clopen set `t` of type `α`, either `s` is a subset of `t` or they are disjoint.
|
IsPreconnected.subset_connectedComponentIn
theorem IsPreconnected.subset_connectedComponentIn :
∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α} {x : α} {F : Set α},
IsPreconnected s → x ∈ s → s ⊆ F → s ⊆ connectedComponentIn F x
This theorem states that for any type `α` with a topological structure, given a preconnected subset `s` of `α`, a point `x` in `s`, and another set `F` in `α` that contains `s`, the set `s` is a subset of the connected component of `x` in `F`. Here, the connected component of `x` in `F` is defined as the connected component of `x` in the subtype `F` seen as a set in `α`, returning the empty set if `x` is not in `F`. The notion of a preconnected set is defined as a set where there is no non-trivial open partition. Therefore, this theorem asserts the relation between preconnected sets and connected components in a topological space.
More concisely: For any topological space `α` with a preconnected subset `s` and a point `x` in `s`, the connected component of `x` in `α` contains `s`.
|
IsPreconnected.closure
theorem IsPreconnected.closure :
∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsPreconnected s → IsPreconnected (closure s)
The theorem `IsPreconnected.closure` states that in any topological space, the closure of a preconnected set is also preconnected. Here, a set is called preconnected if there is no non-trivial partition of it into two open sets. The closure of a set is defined as the smallest closed set that contains it. The theorem implies that the preconnectedness property is preserved under the operation of taking closures in a topological space.
More concisely: In any topological space, the closure of a preconnected set is also preconnected.
|
IsPreconnected.subset_left_of_subset_union
theorem IsPreconnected.subset_left_of_subset_union :
∀ {α : Type u} [inst : TopologicalSpace α] {s u v : Set α},
IsOpen u → IsOpen v → Disjoint u v → s ⊆ u ∪ v → (s ∩ u).Nonempty → IsPreconnected s → s ⊆ u
This theorem states that for any type `α` equipped with a topological space structure, given sets `s`, `u`, and `v` such that `u` and `v` are open sets and disjoint, if `s` is a subset of the union of `u` and `v`, and the intersection of `s` and `u` is nonempty, then if `s` is a preconnected set, it must be a subset of `u`. In essence, if a preconnected set `s` lies within the union of two disjoint open sets `u` and `v` and overlaps with `u`, then `s` must be entirely contained within `u`.
More concisely: If `α` is a topological space, `s` is a preconnected subset of `α`, `u` and `v` are disjoint open sets such that `s ⊆ u ∪ v` and `s ∩ u` is nonempty, then `s ⊆ u`.
|
isConnected_range
theorem isConnected_range :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : ConnectedSpace α]
{f : α → β}, Continuous f → IsConnected (Set.range f)
The theorem `isConnected_range` states that for all types `α` and `β`, given that `α` is endowed with a topological space structure, `β` is also endowed with a topological space structure, and `α` is a connected space, if we have a continuous function `f` from `α` to `β`, then the range of `f` (which is a set of `β` elements) is a connected set. In other words, the continuous image of a connected space is also connected.
More concisely: If `α` is a connected topological space and `f:` `α` `->` `β` is a continuous function, then the range `f''(α)` of `f` is a connected subset of `β`.
|
IsPreconnected.sUnion_directed
theorem IsPreconnected.sUnion_directed :
∀ {α : Type u} [inst : TopologicalSpace α] {S : Set (Set α)},
DirectedOn (fun x x_1 => x ⊆ x_1) S → (∀ s ∈ S, IsPreconnected s) → IsPreconnected S.sUnion
The theorem `IsPreconnected.sUnion_directed` states that for any type `α` with a given topological space structure, if we have a set `S` of subsets of `α`, and the set `S` is directed in the sense that for any two subsets in `S`, there is a third subset in `S` that includes both of them, and every subset in `S` is preconnected (i.e., there is no non-trivial open partition of the subset), then the union of all subsets in `S` is also preconnected. In other words, the directed union of a collection of preconnected subsets is also preconnected.
More concisely: If every subset in a directed family of preconnected subsets of a topological space has no non-trivial open partitions, then their union is also preconnected.
|
ConnectedComponents.surjective_coe
theorem ConnectedComponents.surjective_coe :
∀ {α : Type u} [inst : TopologicalSpace α], Function.Surjective ConnectedComponents.mk
This theorem states that for all types `α` equipped with a topological space structure, the function `ConnectedComponents.mk`, which maps each element of the type `α` to the set of its connected components, is surjective. In other words, for any given connected component in the topological space `α`, there exists an element in `α` which maps to that component under the function `ConnectedComponents.mk`. Thus, every connected component can be reached by this function from some element of the type `α`.
More concisely: For any topological space `α`, the function `ConnectedComponents.mk` maps every connected component to some element in `α`.
|
IsPreconnected.induction₂
theorem IsPreconnected.induction₂ :
∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
IsPreconnected s →
∀ (P : α → α → Prop),
(∀ x ∈ s, ∀ᶠ (y : α) in nhdsWithin x s, P x y) →
(∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z) →
(∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x) → ∀ {x y : α}, x ∈ s → y ∈ s → P x y
The theorem `IsPreconnected.induction₂` can be described as follows:
In the context of a topological space, if you have a preconnected set `s`, and you have a symmetric transitive relation `P` with the property that for any `x` in `s`, `P x y` is true for `y` in a neighborhood within `s` of `x`, then `P x y` holds for all `x, y` in `s`. This is essentially stating that if an equivalence relation has open classes in a preconnected set, then it effectively has a single equivalence class.
More concisely: In a preconnected topological space, if every point has symmetric and transitive neighboring relations in a set such that each relation's closure is connected, then the set is a single equivalence class under that relation.
|
IsConnected.biUnion_of_reflTransGen
theorem IsConnected.biUnion_of_reflTransGen :
∀ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_3} {t : Set ι} {s : ι → Set α},
t.Nonempty →
(∀ i ∈ t, IsConnected (s i)) →
(∀ i ∈ t, ∀ j ∈ t, Relation.ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j) →
IsConnected (⋃ n ∈ t, s n)
This theorem states that the union of a family of connected sets is also connected if the graph determined by whether two sets in the family intersect is preconnected. Here, the term "family of connected sets" refers to a collection of sets indexed by a set `ι`, where each set `s i` in the family is connected. The requirement that this graph of intersections be preconnected essentially means that for any two sets `s i` and `s j` in the family, there's a sequence of sets in the family starting at `s i` and ending at `s j` such that each set in the sequence intersects with the next one.
More concisely: If the graph of intersections of a family of connected sets is preconnected, then the union of this family is connected.
|
IsPreconnected.subset_isClopen
theorem IsPreconnected.subset_isClopen :
∀ {α : Type u} [inst : TopologicalSpace α] {s t : Set α},
IsPreconnected s → IsClopen t → (s ∩ t).Nonempty → s ⊆ t
The theorem `IsPreconnected.subset_isClopen` states that for any type `α` with a topological space structure, and for any sets `s` and `t` of this type, if `s` is a preconnected set and `t` is a clopen (both closed and open) set such that the intersection of `s` and `t` is nonempty (i.e., there is at least one element common to both sets), then `s` is a subset of `t`. In other words, a preconnected set is either contained in or disjoint from any given clopen set.
More concisely: If `α` is a topological space, `s` is a preconnected subset of `α`, `t` is a clopen subset of `α` with nonempty intersection with `s`, then `s` is a subset of `t`.
|
connectedComponent_subset_iInter_isClopen
theorem connectedComponent_subset_iInter_isClopen :
∀ {α : Type u} [inst : TopologicalSpace α] {x : α}, connectedComponent x ⊆ ⋂ Z, ↑Z
The theorem states that, for any given point in a topological space, the connected component of that point is always a subset of the intersection of all its clopen (both closed and open) neighborhoods. In other words, if you take a point and find all the connected sets that contain this point, and then take the union of these connected sets, this resulting set will always be a subset of the intersection of all the clopen neighborhoods of the given point.
More concisely: For any point in a topological space, the connected component of that point is a subset of the intersection of all its clopen neighborhoods.
|
PreconnectedSpace.induction₂
theorem PreconnectedSpace.induction₂ :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : PreconnectedSpace α] (P : α → α → Prop),
(∀ (x : α), ∀ᶠ (y : α) in nhds x, P x y) → Transitive P → Symmetric P → ∀ (x y : α), P x y
This theorem states that in a preconnected topological space, if a symmetric and transitive relation `P` holds for points `y` that are close enough to a point `x` (in the sense that `y` is within a neighborhood of `x`), then the relation `P` holds for all pairs of points `(x, y)` in the space. This is a variant of the concept that if an equivalence relation has open equivalence classes in a topological space, then it only has a single equivalence class. "Close enough" here refers to the mathematical concept of a neighborhood, which in a topological context is a set containing an open set around a given point.
More concisely: In a preconnected topological space, if a symmetric and transitive relation holds between points within neighborhoods of another point, then the relation holds between all pairs of points in the space.
|
connectedComponent_eq
theorem connectedComponent_eq :
∀ {α : Type u} [inst : TopologicalSpace α] {x y : α},
y ∈ connectedComponent x → connectedComponent x = connectedComponent y
This theorem states that for any topological space `α` and any two points `x` and `y` in `α`, if `y` is in the connected component of `x`, then the connected component of `x` is equal to the connected component of `y`. In simpler terms, it means that if two points belong to the same connected component in a topological space, they share the same connected component.
More concisely: For any topological space `α` and points `x, y ∈ α`, if `y` is in the connected component of `x`, then the connected component of `x` equals the connected component of `y`.
|
IsPreconnected.biUnion_of_reflTransGen
theorem IsPreconnected.biUnion_of_reflTransGen :
∀ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_3} {t : Set ι} {s : ι → Set α},
(∀ i ∈ t, IsPreconnected (s i)) →
(∀ i ∈ t, ∀ j ∈ t, Relation.ReflTransGen (fun i j => (s i ∩ s j).Nonempty ∧ i ∈ t) i j) →
IsPreconnected (⋃ n ∈ t, s n)
The theorem `IsPreconnected.biUnion_of_reflTransGen` states that for any type `α` with a topological space structure, and any set `t` of another type `ι`, if each element `i` of `t` indexes a preconnected set `s i` in the space, and furthermore for any two elements `i` and `j` in `t`, there exists a reflexivity-transitive relation that indicates the intersection of the sets they index is not empty and `i` belongs to `t`, then the union of all sets indexed by elements in `t` is also preconnected. This theorem can be interpreted as describing a certain condition under which the union of a family of preconnected sets remains preconnected.
More concisely: If for each index `i` in a set `t`, `s i` is a preconnected subset of a topological space `α`, and there exists a reflexivity-transitive relation connecting any pair of indices `i` and `j` such that the intersection of `s i` and `s j` is non-empty, then the union of all `s i` is preconnected.
|
IsClopen.biUnion_connectedComponent_eq
theorem IsClopen.biUnion_connectedComponent_eq :
∀ {α : Type u} [inst : TopologicalSpace α] {Z : Set α}, IsClopen Z → ⋃ x ∈ Z, connectedComponent x = Z
This theorem states that for any type `α` with a topological structure, given a set `Z` of this type, if `Z` is clopen (both closed and open), then `Z` equals the union of its connected components. In other words, we can construct `Z` by taking every point `x` in `Z` and forming the maximal connected set that includes `x` (the "connected component" of `x`), and then taking the union of all these connected components. This holds for all clopen sets in a general topological space.
More concisely: A clopen set in a topological space is equal to the union of its connected components.
|
PreconnectedSpace.isPreconnected_univ
theorem PreconnectedSpace.isPreconnected_univ :
∀ {α : Type u} [inst : TopologicalSpace α] [self : PreconnectedSpace α], IsPreconnected Set.univ
The theorem `PreconnectedSpace.isPreconnected_univ` states that the universal set, denoted by `Set.univ`, in a preconnected space is a preconnected set. Here, a preconnected space is a topological space that can't be represented as a union of two disjoint nonempty open sets. Hence, in any preconnected topological space, no non-trivial open partition exists for the universal set, which means it is preconnected. The universal set in this context refers to the set containing all elements of the given type, akin to the entire space in topological terms.
More concisely: In a preconnected topological space, the universal set is a preconnected set.
|
preconnectedSpace_of_forall_constant
theorem preconnectedSpace_of_forall_constant :
∀ {α : Type u} [inst : TopologicalSpace α],
(∀ (f : α → Bool), Continuous f → ∀ (x y : α), f x = f y) → PreconnectedSpace α
This theorem, `preconnectedSpace_of_forall_constant`, establishes that any topological space is a preconnected space if all continuous functions from that space to the boolean values are constant. Specifically, for any topological space `α`, if for every continuous function `f` mapping `α` to `Bool`, and for any `x` and `y` in `α`, `f(x)` equals `f(y)`, then `α` is a preconnected space.
More concisely: A topological space is preconnected if every continuous function from the space to the boolean values is constant.
|
isPreconnected_iff_subset_of_disjoint_closed
theorem isPreconnected_iff_subset_of_disjoint_closed :
∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
IsPreconnected s ↔ ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
The theorem `isPreconnected_iff_subset_of_disjoint_closed` states that, for any set `s` in a given topological space, `s` is preconnected if and only if for every pair of closed sets `u` and `v` such that `s` is a subset of the union of `u` and `v` and `s` intersects the intersection of `u` and `v` only at the empty set, then `s` is a subset of either `u` or `v`. In simpler words, a set is preconnected if, whenever it is covered by two closed sets that do not overlap on the set, it must be contained entirely within one of the two covering sets.
More concisely: A set is preconnected if and only if it is a subset of one of two closed sets that have empty intersection and whose union contains the set.
|
preimage_connectedComponent_connected
theorem preimage_connectedComponent_connected :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
(∀ (t : β), IsConnected (f ⁻¹' {t})) →
(∀ (T : Set β), IsClosed T ↔ IsClosed (f ⁻¹' T)) → ∀ (t : β), IsConnected (f ⁻¹' connectedComponent t)
The theorem `preimage_connectedComponent_connected` states that for any types `α` and `β` equipped with topological spaces, and for any function `f` from `α` to `β`, if for every element `t` of `β`, the preimage of the singleton set `{t}` under `f` is a connected set, and for every set `T` of `β`, `T` is closed if and only if its preimage under `f` is closed, then for any `t` in `β`, the preimage of the connected component of `t` under `f` is also connected. In simple terms, if the function `f` preserves the connectedness of singleton sets and the closedness of sets, it also preserves the connectedness of connected components.
More concisely: If a continuous function between topological spaces preserves the connectedness of singletons and the closedness of sets, then it preserves the connectedness of connected components.
|
subsingleton_of_disjoint_isOpen_iUnion_eq_univ
theorem subsingleton_of_disjoint_isOpen_iUnion_eq_univ :
∀ {α : Type u} {ι : Type u_1} [inst : TopologicalSpace α] [inst_1 : PreconnectedSpace α] {s : ι → Set α},
(∀ (i : ι), (s i).Nonempty) →
Pairwise (Disjoint on s) → (∀ (i : ι), IsOpen (s i)) → ⋃ i, s i = Set.univ → Subsingleton ι
This theorem states that in a preconnected topological space, if we have a collection of non-empty open subsets that are pairwise disjoint and their union covers the entire space, then this collection can have at most one element. In other words, in a preconnected space, you cannot cover the whole space with more than one disjoint open set.
More concisely: In a preconnected topological space, the union of a finite collection of pairwise disjoint, non-empty open sets is at most equal to the space if and only if there is exactly one such set.
|
connectedComponentIn_subset
theorem connectedComponentIn_subset :
∀ {α : Type u} [inst : TopologicalSpace α] (F : Set α) (x : α), connectedComponentIn F x ⊆ F
This theorem states that for any type `α` and any topological space `α`, for any set `F` of type `α` and any point `x` of type `α`, the connected component of `x` in `F` is always a subset of `F`. In other words, any element of the connected component of `x` in `F` is also an element of `F`. Here, `connectedComponentIn F x` refers to the set of all points in `F` that are in the same connected component as `x` in the topology of `F`. If `x` is not an element of `F`, the connected component of `x` in `F` is defined to be the empty set, which is trivially a subset of `F`.
More concisely: For any topological space `α`, type `α`, set `F ⊆ α`, and point `x ∈ α`, the connected component of `x` in `F`, `connectedComponentIn F x`, is a subset of `F`.
|
isClopen_iff
theorem isClopen_iff :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : PreconnectedSpace α] {s : Set α},
IsClopen s ↔ s = ∅ ∨ s = Set.univ
The theorem `isClopen_iff` states that for any type `α` equipped with a topology and assumed to be preconnected, and any set `s` of type `α`, the statement "The set `s` is clopen" is equivalent to "The set `s` is either empty or equal to the universal set of `α`". Here, a set is defined to be clopen if it is both closed and open in the given topological space. This theorem essentially says that in a preconnected topological space, the only clopen sets are the empty set and the entire space itself.
More concisely: In a preconnected topological space, a set is clopen if and only if it is either the empty set or the universal set.
|
isConnected_iff_sUnion_disjoint_open
theorem isConnected_iff_sUnion_disjoint_open :
∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
IsConnected s ↔
∀ (U : Finset (Set α)),
(∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
(∀ u ∈ U, IsOpen u) → s ⊆ (↑U).sUnion → ∃ u ∈ U, s ⊆ u
The theorem `isConnected_iff_sUnion_disjoint_open` states that a set `s` is connected, in the context of a topological space, if and only if for every covering of `s` by a finite collection of open sets that are pairwise disjoint on `s`, `s` is contained in one of the sets in the collection. Here, "pairwise disjoint on `s`" means that for any two different sets `u` and `v` in the collection, their intersection with `s` is not nonempty unless `u` and `v` are the same set.
More concisely: A topological space's subsets s is connected if and only if it is contained in at least one set of a finite, pairwise disjoint open cover of s.
|
PreconnectedSpace.induction₂'
theorem PreconnectedSpace.induction₂' :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : PreconnectedSpace α] (P : α → α → Prop),
(∀ (x : α), ∀ᶠ (y : α) in nhds x, P x y ∧ P y x) → Transitive P → ∀ (x y : α), P x y
The theorem states that in a preconnected topological space, if there exists a transitive relation `P` such that `P x y` and `P y x` hold true for all `y` that are sufficiently close to `x` (i.e., `y` is in the neighborhood of `x`), then `P x y` must hold true for all pairs `x, y` in the space. This theorem is a variant of the fact that if an equivalence relation has open equivalence classes in a topological space, then there exists only a single equivalence class.
More concisely: In a preconnected topological space, if a transitive relation has symmetric neighborhood relations, then it is an equivalence relation.
|
IsPreconnected.induction₂'
theorem IsPreconnected.induction₂' :
∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
IsPreconnected s →
∀ (P : α → α → Prop),
(∀ x ∈ s, ∀ᶠ (y : α) in nhdsWithin x s, P x y ∧ P y x) →
(∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z) → ∀ {x y : α}, x ∈ s → y ∈ s → P x y
This theorem states that in a preconnected set, given a transitive relation `P`, if `P x y` and `P y x` hold true for `y` within a neighborhood of `x` in the set, then `P x y` holds true for all pairs of `x, y` in the set.
In other words, it states that if an equivalence relation whose classes are open sets in a topological space is reflexive and symmetric in a neighborhood of each point in a preconnected set, and is transitive on the entire preconnected set, then this equivalence relation holds true for all pairs of points within the preconnected set. This theorem is an instantiation of the concept that if an equivalence relation has open classes in a preconnected space, then it has a single equivalence class.
More concisely: In a preconnected set, if an equivalence relation with open classes is transitive and satisfies symmetry in a neighborhood of each point, then it is equalitie-reflexive on the entire set. (Note: This statement assumes that the preconnected set is endowed with a topology such that the equivalence classes are open sets.)
|
Continuous.exists_lift_sigma
theorem Continuous.exists_lift_sigma :
∀ {α : Type u} {ι : Type u_1} {π : ι → Type u_2} [inst : TopologicalSpace α] [inst_1 : ConnectedSpace α]
[inst_2 : (i : ι) → TopologicalSpace (π i)] {f : α → (i : ι) × π i},
Continuous f → ∃ i g, Continuous g ∧ f = Sigma.mk i ∘ g
This theorem states that if there is a continuous map `f` from a connected topological space `α` to a disjoint union (denoted as `Σ i, π i` in Lean 4), then it's possible to "lift" this map to a map `g` onto one of the components `π i` of the disjoint union. In other words, there exists an index `i` and a continuous function `g` such that `f` is equivalent to applying `g` first and then mapping onto `π i`. There is another similar theorem `ContinuousMap.exists_lift_sigma` for the case when maps are bundled as `ContinuousMap`.
More concisely: Given a continuous function `f` from a connected topological space `α` to a disjoint union `Σ i, π i`, there exists an index `i` and a continuous function `g` such that `f` is equivalent to the composition of `g` and the projection `π i`.
|
isPreconnected_connectedComponent
theorem isPreconnected_connectedComponent :
∀ {α : Type u} [inst : TopologicalSpace α] {x : α}, IsPreconnected (connectedComponent x)
This theorem states that, for any type `α` with a topological space structure and for any point `x` in `α`, the connected component of `x` is a preconnected set. In mathematical terms, the connected component of a point, which is the largest set containing the point where there is no non-trivial open partition, is always preconnected. This means that for any two open sets `u` and `v`, if the connected component of `x` is a subset of the union of `u` and `v` and has nonempty intersection with both `u` and `v`, then it also has nonempty intersection with the intersection of `u` and `v`.
More concisely: For any topological space `(α, τ)` and point `x` in `α`, the connected component of `x` is a preconnected set, i.e., if it intersects both open sets `u` and `v` non-empty and is a subset of their union, then it also intersects their intersection non-empty.
|
IsPreconnected.subset_closure
theorem IsPreconnected.subset_closure :
∀ {α : Type u} [inst : TopologicalSpace α] {s t : Set α},
IsPreconnected s → s ⊆ t → t ⊆ closure s → IsPreconnected t
The theorem of bark and tree states the following: for any topological space, if you have a preconnected set and another set that is a subset of both this preconnected set and its closure, then this second set is also preconnected. In other words, being completely contained within a preconnected set and its closure is enough to guarantee that a set is also preconnected. See also the theorem `IsConnected.subset_closure` for a related result.
More concisely: If a set is both a subset of a preconnected set and its closure in a topological space, then the set is preconnected.
|
IsPreirreducible.isPreconnected
theorem IsPreirreducible.isPreconnected :
∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsPreirreducible s → IsPreconnected s
The theorem `IsPreirreducible.isPreconnected` states that for any type `α` equipped with a topological structure, and for any set `s` of type `α`, if `s` is preirreducible (which means that there are no non-trivial pairs of disjoint open sets within `s`), then `s` is also preconnected. In the context of topology, a preconnected set is one where there is no non-trivial open partition. In other words, a preirreducible set in a topological space is always preconnected within that space.
More concisely: A preirreducible set in a topological space is preconnected.
|
IsPreconnected.iUnion_of_chain
theorem IsPreconnected.iUnion_of_chain :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] [inst_2 : SuccOrder β]
[inst_3 : IsSuccArchimedean β] {s : β → Set α},
(∀ (n : β), IsPreconnected (s n)) → (∀ (n : β), (s n ∩ s (Order.succ n)).Nonempty) → IsPreconnected (⋃ n, s n)
The theorem `IsPreconnected.iUnion_of_chain` states that for any two types `α` and `β`, where `α` is a topological space, `β` is a linear ordered type and has a successor operation. If `β` has the Archimedean property, which means that there is no infinite gap in `β`, and `s` is a function from `β` to a set of `α`, such that each set `s(n)` is preconnected and any two neighboring sets `s(n)` and `s(n+1)` have a non-empty intersection, then the union of all these sets `s(n)` is also preconnected.
In other words, if we have a chain of connected sets (meaning each set is connected with its successor in the chain), where the chain index type has no infinite gaps (like integers or natural numbers), then the entire union of these sets is preconnected.
More concisely: If `α` is a topological space, `β` is a linearly ordered type with the Archimedean property, and `s : β → α` is a function such that each `s(n)` is preconnected and `s(n) ∩ s(n+1) ≠ ∅`, then the union of the `s(n)`'s is preconnected.
|
isPreconnected_empty
theorem isPreconnected_empty : ∀ {α : Type u} [inst : TopologicalSpace α], IsPreconnected ∅
The theorem `isPreconnected_empty` asserts that for any type `α` equipped with a topology (i.e., a topological space), the empty set `∅` is preconnected. According to the provided definition, a set is preconnected if it does not have a non-trivial open partition. The theorem thus states that the empty set does not have such a partition, making it preconnected in any topological space.
More concisely: In any topological space, the empty set is preconnected, that is, it does not have a non-trivial open partition.
|
IsClopen.eq_univ
theorem IsClopen.eq_univ :
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : PreconnectedSpace α] {s : Set α},
IsClopen s → s.Nonempty → s = Set.univ
This theorem states that for any type `α` equipped with a topology and a preconnected space structure, if a set `s` of `α` is clopen (both closed and open) and nonempty, then `s` is equal to the universal set. This means that in a preconnected space, any nonempty clopen set must include all elements of the space.
More concisely: In a preconnected topological space, any nonempty clopen set is equal to the universal set.
|
IsConnected.subset_closure
theorem IsConnected.subset_closure :
∀ {α : Type u} [inst : TopologicalSpace α] {s t : Set α}, IsConnected s → s ⊆ t → t ⊆ closure s → IsConnected t
The "Theorem of bark and tree" states that for any set `t` within a connected set `s` and its closure in a topological space `α`, `t` is also a connected set. In other words, if a set `s` is connected, and another set `t` is a subset of both `s` and the closure of `s`, then `t` is also connected. The closure of a set is the smallest closed set containing the given set. This is a property of connectedness in topological spaces.
More concisely: If a connected set `s` in a topological space contains its subset `t` and the closure of `t` is included in `s`, then `t` is also connected.
|
IsPreconnected.iUnion_of_reflTransGen
theorem IsPreconnected.iUnion_of_reflTransGen :
∀ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_3} {s : ι → Set α},
(∀ (i : ι), IsPreconnected (s i)) →
(∀ (i j : ι), Relation.ReflTransGen (fun i j => (s i ∩ s j).Nonempty) i j) → IsPreconnected (⋃ n, s n)
The theorem `IsPreconnected.iUnion_of_reflTransGen` states that in a topological space `α`, the indexed union of a family of preconnected sets, where the sets are indexed by the vertices of a preconnected graph, is also preconnected if the following conditions hold:
1. Each set in the family is preconnected.
2. Any two vertices in the graph (which corresponds to the indices of the sets) are connected by a sequence of hops (A hop is a path from one vertex to another vertex) in which consecutive vertices correspond to intersecting sets (i.e., there exists an element common to both sets).
In other words, if we have a collection of preconnected sets that are "linked" together in the sense that you can find a chain of sets where each intersects with the next one, then the union of all these sets is also preconnected.
More concisely: Given a preconnected graph with vertices indexing a family of preconnected subsets of a topological space such that any pair of connected vertices is linked by a chain of intersecting sets, the indexed union of these sets is preconnected.
|
Inducing.isPreconnected_image
theorem Inducing.isPreconnected_image :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {f : α → β},
Inducing f → (IsPreconnected (f '' s) ↔ IsPreconnected s)
The theorem `Inducing.isPreconnected_image` states that for any two types `α` and `β` (with `α` and `β` being any mathematical objects such as sets or numbers), both equipped with a topological space structure (a notion of "closeness" or "continuity"), a set `s` of type `α`, and a function `f` from `α` to `β`, if the function `f` induces the topology from `α` to `β` (i.e., the "closeness" structure in `β` is the same as the "closeness" structure in `α` when mapped by `f`), then the image of the set `s` under the function `f` is preconnected (i.e., cannot be split into two non-empty open sets) if and only if the original set `s` is preconnected. In simpler terms, the theorem says that a continuous mapping preserves the property of being preconnected.
More concisely: If a continuous function preserves the topology between two spaces, then the image of a preconnected set is a preconnected set.
|
IsConnected.iUnion_of_chain
theorem IsConnected.iUnion_of_chain :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] [inst_2 : SuccOrder β]
[inst_3 : IsSuccArchimedean β] [inst_4 : Nonempty β] {s : β → Set α},
(∀ (n : β), IsConnected (s n)) → (∀ (n : β), (s n ∩ s (Order.succ n)).Nonempty) → IsConnected (⋃ n, s n)
The theorem `IsConnected.iUnion_of_chain` states that if we have a collection of connected sets, each indexed by a type that has an Archimedean successor (like the natural numbers `ℕ` or integers `ℤ`), and if every two consecutive sets in this collection have a non-empty intersection, then the union of all these sets is also a connected set. This is under the context of a topological space. This theorem essentially describes a property of connectedness preservation under certain conditions in the context of topological spaces.
More concisely: If $(X, \tau)$ is a topological space, $I$ is a type with an Archimedean successor, and for all $i, j \in I$, $i < j$ implies $X\_i \cap X\_j \neq \emptyset$, then $\bigcup\_{i \in I} X\_i$ is connected.
|
isPreconnected_sUnion
theorem isPreconnected_sUnion :
∀ {α : Type u} [inst : TopologicalSpace α] (x : α) (c : Set (Set α)),
(∀ s ∈ c, x ∈ s) → (∀ s ∈ c, IsPreconnected s) → IsPreconnected c.sUnion
The theorem `isPreconnected_sUnion` states that if we have a family of sets in a topological space, where each of the sets is preconnected and they all have a common point, then the union of these sets is also preconnected. In other words, if for all sets in a collection `c`, a point `x` is contained in the set and the set is preconnected, then the union over this collection `c` is also preconnected.
More concisely: If every set in a family has a common point and is preconnected, then the union of the sets is preconnected.
|
IsConnected.nonempty
theorem IsConnected.nonempty : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsConnected s → s.Nonempty := by
sorry
This theorem, named `IsConnected.nonempty`, states that for any set `s` of a certain type `α` in a topological space, if `s` is a connected set, then `s` is not empty. In other words, the theorem asserts that a connected set must contain at least one element. It can be seen as a property of connected sets in the context of topology.
More concisely: In a topological space, a connected set is non-empty.
|
isConnected_connectedComponent
theorem isConnected_connectedComponent :
∀ {α : Type u} [inst : TopologicalSpace α] {x : α}, IsConnected (connectedComponent x)
The theorem `isConnected_connectedComponent` states that for any type `α` with a given topological space structure and for any point `x` of this type, the connected component of `x` is a connected set. The connected component of a point is defined as the maximal set containing this point that cannot be divided into two nonempty open sets without intersection. A set is defined as connected if it is nonempty and does not allow a non-trivial open partition.
More concisely: For any topological space `(α, top)` and point `x ∈ α`, the connected component of `x` is a connected subset of `α`.
|
connectedComponentIn_eq_image
theorem connectedComponentIn_eq_image :
∀ {α : Type u} [inst : TopologicalSpace α] {F : Set α} {x : α} (h : x ∈ F),
connectedComponentIn F x = Subtype.val '' connectedComponent ⟨x, h⟩
This theorem states that in any topological space `α`, for any subset `F` of `α` and a point `x` in `α` such that `x` belongs to `F`, the connected component of `x` in `F` is equivalent to the image under the subtype value function of the connected component of the subtype `{ val := x, property := h }`. Here, `h` is the assumption that `x` is in `F`. In other words, if a point belongs to a set in a topological space, its connected component within that set is the same as the connected component of the point considered as an element of the subtype defined by the set.
More concisely: In any topological space, the connected component of a point in a subset is equal to the image under the subtype value function of the connected component of the subpoint.
|
IsClopen.connectedComponent_subset
theorem IsClopen.connectedComponent_subset :
∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α} {x : α}, IsClopen s → x ∈ s → connectedComponent x ⊆ s := by
sorry
This theorem states that for any type `α` endowed with a topological space structure and any subset `s` of `α` that is clopen (both closed and open), if a point `x` is a member of `s`, then the connected component of `x` is a subset of `s`. The connected component of a point is the largest preconnected set containing that point. In the context of topological spaces, a set is preconnected if it cannot be represented as the union of two disconnected non-empty open sets.
More concisely: If `α` is a topological space, `s` is a clopen subset of `α`, and `x` is an element of `s`, then the connected component of `x` is contained in `s`.
|
Sigma.isConnected_iff
theorem Sigma.isConnected_iff :
∀ {ι : Type u_1} {π : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (π i)] {s : Set ((i : ι) × π i)},
IsConnected s ↔ ∃ i t, IsConnected t ∧ s = Sigma.mk i '' t
The theorem `Sigma.isConnected_iff` states that for any set `s` of pairs (also known as a sigma type), where the first element of the pair is of type `ι` and the second element is of a type `π i` that depends on `ι`, and each `π i` is equipped with a topological structure, the set `s` is connected if and only if there exists an index `i` and a set `t` such that `t` is connected and `s` is the image of `t` under the function `Sigma.mk i`. Here, the function `Sigma.mk i` creates pairs where the first element is `i` and the second element is from `t`. The connectedness of a set is defined as the set being nonempty and there is no non-trivial open partition.
More concisely: A sigma type of pairs, where the first element is of type `ι` and the second element is of a connected type `π i`, is connected if and only if it is the image of a connected set under the function that maps each element to a pair with the first element being a fixed index and the second element from the set.
|
isPreconnected_of_forall
theorem isPreconnected_of_forall :
∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α} (x : α),
(∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t) → IsPreconnected s
The theorem `isPreconnected_of_forall` states that for any set `s` of a type `α` with a topological space structure, and any fixed point `x`, if for every point `y` in `s`, there exists a preconnected subset `t` of `s` such that `x` and `y` are in `t`, then the original set `s` is preconnected. In terms of topology, this implies that if all points in a set can be connected to a particular one via a preconnected path, the set itself must be preconnected.
More concisely: If for every pair of points in a pretopology-equipped set, there exists a preconnected sub-set containing them, then the set is preconnected.
|
IsConnected.closure
theorem IsConnected.closure :
∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsConnected s → IsConnected (closure s)
The theorem `IsConnected.closure` states that for any topological space `α` and a set `s` within this space, if the set `s` is connected (i.e., it's nonempty and there's no non-trivial open partition), then the closure of this set is also connected. The closure of a set `s` is the smallest closed set that contains `s`. This theorem is a property of general topological spaces and is not specific to any particular kind of space such as metric spaces or Euclidean spaces.
More concisely: If a connected set `s` in a topological space `α` has closure `cl(s)`, then `cl(s)` is also a connected set.
|
isPreconnected_iff_subset_of_disjoint
theorem isPreconnected_iff_subset_of_disjoint :
∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
IsPreconnected s ↔ ∀ (u v : Set α), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
The theorem `isPreconnected_iff_subset_of_disjoint` states that a set `s` in a topological space `α` is preconnected if and only if for every pair of open sets `u` and `v` such that `s` is covered by `u` union `v` and `s` intersects the intersection of `u` and `v` only at the empty set, then `s` is a subset of either `u` or `v`. In other words, a set in a topological space is preconnected if it cannot be split into two disjoint open sets; it is entirely contained within one or the other open set for any such disjoint partition.
More concisely: A set in a topological space is preconnected if and only if it does not intersect the intersection of any two open sets containing it only in their empty intersection.
|
ConnectedSpace.toNonempty
theorem ConnectedSpace.toNonempty : ∀ {α : Type u} [inst : TopologicalSpace α] [self : ConnectedSpace α], Nonempty α
This theorem states that any connected space is nonempty. In more detail, for any given type `α` and assuming `α` is a topological space and a connected space, there is at least one element in `α`. This is a fundamental property of connected spaces in topology.
More concisely: Every connected topological space is nonempty.
|
IsPreconnected.biUnion_of_chain
theorem IsPreconnected.biUnion_of_chain :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] [inst_2 : SuccOrder β]
[inst_3 : IsSuccArchimedean β] {s : β → Set α} {t : Set β},
t.OrdConnected →
(∀ n ∈ t, IsPreconnected (s n)) →
(∀ n ∈ t, Order.succ n ∈ t → (s n ∩ s (Order.succ n)).Nonempty) → IsPreconnected (⋃ n ∈ t, s n)
This theorem states that the union of a sequence of preconnected sets, indexed by a subset of a type with an Archimedean successor operation (like natural numbers `ℕ` or integers `ℤ`), is itself preconnected, under certain conditions. These conditions are: first, that the indexing set forms an ordered set without any gaps; second, that each set in the sequence is preconnected; and third, that any two subsequent sets in the sequence have a nonempty intersection. In mathematical terms, if `t` is an ordered, gap-less subset of `β` (where `β` has an Archimedean successor operation), and `s` is a sequence of preconnected sets such that for every `n` in `t`, `s n` and `s (succ n)` intersect, then the union of the `s n` for `n` in `t` is preconnected.
More concisely: If `t` is a gap-less, ordered subset of a type `β` with an Archimedean successor operation, and `s` is a sequence of preconnected sets indexed by `t` such that for all `n` in `t`, `s n` and `s (succ n)` intersect, then the union of the `s n` is preconnected.
|
subsingleton_of_disjoint_isClopen
theorem subsingleton_of_disjoint_isClopen :
∀ {α : Type u} {ι : Type u_1} [inst : TopologicalSpace α] [inst_1 : PreconnectedSpace α] {s : ι → Set α},
(∀ (i : ι), (s i).Nonempty) → Pairwise (Disjoint on s) → (∀ (i : ι), IsClopen (s i)) → Subsingleton ι
The theorem `subsingleton_of_disjoint_isClopen` states that in a preconnected topological space, any family of subsets, where each subset is non-empty and clopen (both closed and open), and where the subsets are pairwise disjoint (meaning that the intersection of any two different subsets is the bottom element), can have at most one element. In other words, if we have a preconnected space and a collection of non-empty, pairwise disjoint clopen subsets of that space, then this collection cannot have more than one element.
More concisely: In a preconnected topological space, there cannot exist more than one non-empty, clopen, and pairwise disjoint subset.
|
connectedComponents_preimage_singleton
theorem connectedComponents_preimage_singleton :
∀ {α : Type u} [inst : TopologicalSpace α] {x : α},
ConnectedComponents.mk ⁻¹' {ConnectedComponents.mk x} = connectedComponent x
This theorem states that for any topological space `α` and any point `x` of `α`, the preimage of the singleton set containing the connected component of `x` under the function `ConnectedComponents.mk` is equal to the connected component of `x`. In simpler terms, this means that the points in the topological space `α` which are identified to the connected component of `x` by `ConnectedComponents.mk` are exactly those in the connected component of `x`. The connected component of `x` is defined as the maximum connected set that contains the point `x`.
More concisely: For any topological space `α` and point `x` in `α`, the preimage of the connected component of `x` under `ConnectedComponents.mk` equals the connected component of `x`. In other words, the points identified to the connected component of `x` by `ConnectedComponents.mk` are precisely the points in the connected component of `x`.
|
IsConnected.image
theorem IsConnected.image :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α},
IsConnected s → ∀ (f : α → β), ContinuousOn f s → IsConnected (f '' s)
This theorem states that if a set is connected in a topological space, then the image of this set under a continuous function is also connected in its respective topological space. In other words, for any topological spaces `α` and `β`, any connected set `s` in `α`, and any function `f: α → β` that is continuous on `s`, the image of `s` under `f` (denoted as `f '' s`) is also connected in `β`. This highlights the preserving nature of continuous functions with respect to the property of connectedness.
More concisely: If `s` is a connected subset of a topological space `α`, and `f: α → β` is a continuous function, then `f '' s` is a connected subset of `β`.
|
connectedComponents_preimage_image
theorem connectedComponents_preimage_image :
∀ {α : Type u} [inst : TopologicalSpace α] (U : Set α),
ConnectedComponents.mk ⁻¹' (ConnectedComponents.mk '' U) = ⋃ x ∈ U, connectedComponent x
The theorem `connectedComponents_preimage_image` states that for any topological space `α` and any set `U` of type `α`, the preimage of the image of `U` under the map to the connected components of `α` is equal to the union of the connected components of the elements in `U`. In other words, if we map `U` to its connected components and then reverse that mapping, we get the union of the maximal connected sets that contain each point in `U`.
More concisely: For any topological space α and subset U, the preimage of the image of U under the connected components map equals the union of the connected components of the points in U.
|
Continuous.image_connectedComponent_subset
theorem Continuous.image_connectedComponent_subset :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
Continuous f → ∀ (a : α), f '' connectedComponent a ⊆ connectedComponent (f a)
This theorem states that for any continuous function `f` from one topological space `α` to another topological space `β`, the image under `f` of the connected component of any point `a` in `α` is a subset of the connected component of the image of the point `f(a)` in `β`. In other words, continuous functions map connected components to subsets of connected components.
More concisely: For any continuous function between topological spaces and any point in the domain, the image of the connected component of that point is contained in the connected component of the image under the function.
|
isPreconnected_iff_subset_of_fully_disjoint_closed
theorem isPreconnected_iff_subset_of_fully_disjoint_closed :
∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
IsClosed s →
(IsPreconnected s ↔ ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → Disjoint u v → s ⊆ u ∨ s ⊆ v)
A set `s` in a topological space `α` is preconnected if and only if the following condition holds: for any two closed sets `u` and `v` that cover `s` and are disjoint (i.e., their intersection is empty), `s` must be entirely contained within either `u` or `v`. This theorem connects the concept of preconnectedness with conditions involving disjoint coverings with closed sets.
More concisely: A set in a topological space is preconnected if and only if any disjoint closed coverings of the set have their union equal to the set.
|
IsConnected.biUnion_of_chain
theorem IsConnected.biUnion_of_chain :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] [inst_2 : SuccOrder β]
[inst_3 : IsSuccArchimedean β] {s : β → Set α} {t : Set β},
t.Nonempty →
t.OrdConnected →
(∀ n ∈ t, IsConnected (s n)) →
(∀ n ∈ t, Order.succ n ∈ t → (s n ∩ s (Order.succ n)).Nonempty) → IsConnected (⋃ n ∈ t, s n)
This theorem, named `IsConnected.biUnion_of_chain`, states that for any types `α` (with a topology) and `β` (with a linear order and a successor operation that satisfies the Archimedean property), given a function `s` from `β` to `set α` and a subset `t` of `β`, if `t` is nonempty and its elements are ordered (i.e., `t` is an ordered chain), every set `s n` for `n` in `t` is connected, and any two neighboring sets `s n` and `s (Order.succ n)` intersect, then the union of all sets `s n` for `n` in `t` is also a connected set.
In other words, if you have a sequence of connected sets indexed by elements of an ordered set (with a successor operation that abides by the Archimedean property) such that any two consecutive sets in this sequence have a nonempty intersection, their union remains connected.
More concisely: If `s` is a function from an ordered set `β` with the Archimedean property to the power set of a topological space `α`, and `t` is a nonempty ordered chain in `β` such that `s n` is connected and intersects `s (Order.succ n)` for all `n` in `t`, then the union of `{s n | n ∈ t}` is connected.
|
subsingleton_of_disjoint_isClosed_iUnion_eq_univ
theorem subsingleton_of_disjoint_isClosed_iUnion_eq_univ :
∀ {α : Type u} {ι : Type u_1} [inst : TopologicalSpace α] [inst_1 : PreconnectedSpace α] {s : ι → Set α},
(∀ (i : ι), (s i).Nonempty) →
Pairwise (Disjoint on s) →
∀ [inst_2 : Finite ι], (∀ (i : ι), IsClosed (s i)) → ⋃ i, s i = Set.univ → Subsingleton ι
This theorem states that in a preconnected topological space, if we have a finite collection of non-empty closed subsets that pairwise disjoint and their union equals the entire space, then the collection can have at most one element. Precisely, if for each index `i` in a finite index set `ι`, the subset `s i` is non-empty and closed, and the subsets `s i` are pairwise disjoint (meaning for any two different indices `i` and `j`, the subsets `s i` and `s j` do not share elements), and the union of all the subsets `s i` is the entire space, then the index set `ι` is a subsingleton, which means it contains at most one element. This is a property of preconnected spaces, which are spaces that cannot be represented as the union of two disjoint, non-empty, open sets. In other words, there is no way to "divide" a preconnected space into two separate parts.
More concisely: In a preconnected topological space, if a finite collection of non-empty closed subsets are pairwise disjoint and their union equals the entire space, then the collection contains at most one element.
|
IsConnected.isPreconnected
theorem IsConnected.isPreconnected :
∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α}, IsConnected s → IsPreconnected s
The theorem `IsConnected.isPreconnected` states that for any type `α` that has a topology (i.e., it is a topological space), and any set `s` of this type, if `s` is a connected set, then `s` is also preconnected. In terms of topology, a connected set is one that cannot be partitioned into two non-empty open sets. This theorem, therefore, establishes that if a set fulfills this condition, it also fulfills the conditions to be preconnected, which implies that there is no non-trivial open partition of the set.
More concisely: If `α` is a topological space and `s` is a connected subset of `α`, then `s` is preconnected.
|
IsPreconnected.image
theorem IsPreconnected.image :
∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α},
IsPreconnected s → ∀ (f : α → β), ContinuousOn f s → IsPreconnected (f '' s)
The theorem `IsPreconnected.image` states that for any two types `α` and `β`, equipped with their respective topological spaces, and for any set `s` of type `α`, if `s` is preconnected and there is a function `f` from `α` to `β` that is continuous on `s`, then the image of `s` under `f` is also preconnected. In simpler terms, this theorem asserts that the continuous image of a preconnected set remains preconnected.
More concisely: If `s` is a preconnected subset of a topological space `(α, τα)`, and `f : α → β` is a continuous function, then the image `f''(s)` is also a preconnected subset of `(β, τβ)`.
|