Set.Countable.isConnected_compl_of_one_lt_rank
theorem Set.Countable.isConnected_compl_of_one_lt_rank :
∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
[inst_3 : ContinuousAdd E] [inst_4 : ContinuousSMul ℝ E],
1 < Module.rank ℝ E → ∀ {s : Set E}, s.Countable → IsConnected sᶜ
The theorem states that in a real vector space of dimension greater than 1, the complement (i.e., all the elements not in the set) of any countable set is connected. Here, a set is considered connected if it is nonempty and if there is no non-trivial open partition of the set. The conditions on the vector space include being equipped with a topological structure, a continuous addition operation and a continuous scalar multiplication operation. The theorem applies to any countable set within this vector space, where a set is countable if it has the same cardinality as some subset of the natural numbers.
More concisely: In a real vector space of dimension greater than 1 endowed with a topology, the complement of any countable set is a connected set.
|
isConnected_compl_singleton_of_one_lt_rank
theorem isConnected_compl_singleton_of_one_lt_rank :
∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
[inst_3 : ContinuousAdd E] [inst_4 : ContinuousSMul ℝ E], 1 < Module.rank ℝ E → ∀ (x : E), IsConnected {x}ᶜ
The theorem states that in a real vector space with dimension greater than 1, the set that is the complement of a singleton set (a set containing only one element) is a connected set. In the context of topology, a connected set is one that is nonempty and cannot be divided into two non-overlapping open sets. This theorem is applicable for any given element in the vector space.
More concisely: In a real vector space of dimension greater than 1, the complement of a singleton set is a connected set.
|
isPathConnected_sphere
theorem isPathConnected_sphere :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
1 < Module.rank ℝ E → ∀ (x : E) {r : ℝ}, 0 ≤ r → IsPathConnected (Metric.sphere x r)
This theorem states that in a real vector space of dimension greater than one, any sphere with a nonnegative radius is path connected. In other words, if we have a vector space over the real numbers with dimension more than one and if we take any point in the space and consider a sphere centered at that point with a nonnegative radius, then there exists a point in this sphere that can be joined to any other point in the sphere via a continuous path that does not leave the sphere.
More concisely: In a real vector space of dimension greater than one, any sphere with a nonnegative radius is path-connected.
|
Set.Countable.isPathConnected_compl_of_one_lt_rank
theorem Set.Countable.isPathConnected_compl_of_one_lt_rank :
∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
[inst_3 : ContinuousAdd E] [inst_4 : ContinuousSMul ℝ E],
1 < Module.rank ℝ E → ∀ {s : Set E}, s.Countable → IsPathConnected sᶜ
This theorem states that in a real vector space of dimension greater than one (`1 < Module.rank ℝ E`), the complement of any countable set (`s.Countable`) is path-connected (`IsPathConnected sᶜ`). Here, a set is path-connected if it contains a point that can be connected to all other points within the set. In this context, a countable set refers to a set that has the same cardinality (size) as some subset of the set of all natural numbers, and the complement of a set includes all elements not in the original set. Moreover, the theorem applies to vector spaces where addition and scalar multiplication are continuous operations.
More concisely: In a real vector space of dimension greater than one and where addition and scalar multiplication are continuous operations, the complement of any countable subset is path-connected.
|
isPathConnected_compl_singleton_of_one_lt_rank
theorem isPathConnected_compl_singleton_of_one_lt_rank :
∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
[inst_3 : ContinuousAdd E] [inst_4 : ContinuousSMul ℝ E], 1 < Module.rank ℝ E → ∀ (x : E), IsPathConnected {x}ᶜ
This theorem states that in a real vector space of dimension greater than 1, the complement of any singleton set is path-connected. Path-connected means that there exists a point in the set such that every other point in the set can be connected to it via a continuous path that lies within the set. Specifically, for any point in the vector space, the set of all other points in the vector space (i.e., the complement of the singleton containing just the given point) is path-connected. This is true for all real vector spaces of dimension more than 1.
More concisely: In a real vector space of dimension greater than 1, the complement of any singleton set is path-connected.
|
isPreconnected_sphere
theorem isPreconnected_sphere :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
1 < Module.rank ℝ E → ∀ (x : E) (r : ℝ), IsPreconnected (Metric.sphere x r)
This theorem states that in a real vector space of dimension greater than 1, any sphere is preconnected. Here, a sphere is defined as the set of all points that are at a specific distance (radius) from a given point (center). Preconnectedness, in this case, is defined as the property such that for any two open sets that cover the set, if they both intersect with the set, they also intersect with each other within the set. Essentially, the theorem says there is no non-trivial way to split a sphere into two separate open sets without overlap.
More concisely: In a real vector space of dimension greater than 1, any sphere is a connected set. (Note: "connected" is synonymous with "preconnected" in the context of topology.)
|
isConnected_sphere
theorem isConnected_sphere :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
1 < Module.rank ℝ E → ∀ (x : E) {r : ℝ}, 0 ≤ r → IsConnected (Metric.sphere x r)
The theorem `isConnected_sphere` states that in any real vector space with dimension greater than 1, any sphere with a nonnegative radius is a connected set. Here, a connected set is defined as a set that is nonempty and does not have a non-trivial open partition, and a sphere centered at a point `x` with radius `r` is defined as the set of all points at a distance `r` from `x`. The dimension of the vector space is represented by the rank of the module, and the requirement that this rank is greater than 1 ensures that the vector space is more than one-dimensional. The radius of the sphere is required to be nonnegative, which means it includes the sphere's center point.
More concisely: In a real vector space of dimension greater than 1, any sphere with a nonnegative radius is a connected set.
|