Joined.trans
theorem Joined.trans : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y z : X}, Joined x y → Joined y z → Joined x z
The theorem `Joined.trans` states that for any topological space `X` and any three points `x`, `y`, and `z` in `X`, if `x` is joined to `y` by a path and `y` is joined to `z` by a path, then `x` is also joined to `z` by a path. This is essentially stating the transitivity of the "being joined by a path" relation in a topological space.
More concisely: If $x$ is connected to $y$ and $y$ is connected to $z$ in a topological space, then $x$ is connected to $z$.
|
Path.ext
theorem Path.ext : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {γ₁ γ₂ : Path x y}, ⇑γ₁ = ⇑γ₂ → γ₁ = γ₂ := by
sorry
This theorem, `Path.ext`, states that for any type `X` that has a `TopologicalSpace` instance and for any two points `x` and `y` in `X`, if we have two paths `γ₁` and `γ₂` from `x` to `y`, and if the continuous maps from the unit interval [0, 1] to `X` induced by `γ₁` and `γ₂` are equal (i.e., `⇑γ₁ = ⇑γ₂`), then the two paths `γ₁` and `γ₂` themselves are equal (i.e., `γ₁ = γ₂`). This theorem basically tells us that the equality of paths in a topological space can be determined by the equality of their induced continuous maps.
More concisely: In a topological space, if two continuous paths from one point to another have equal induced continuous maps from the unit interval, then they are equal as paths.
|
Path.truncate_continuous_family
theorem Path.truncate_continuous_family :
∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b),
Continuous fun x => (γ.truncate x.1 x.2.1) x.2.2
The theorem `Path.truncate_continuous_family` states that for any path `γ` in a topological space `X` which connects points `a` and `b`, the `truncate` function of `γ` generates a continuous family of paths. This is meant in the sense that the uncurried function that maps a tuple `(t₀, t₁, s)` to the path `γ.truncate t₀ t₁ s` is a continuous function.
More concisely: The function that maps a triple `(t₀, t₁, s)` to the truncated path `γ.truncate t₀ t₁ s` of a continuous path `γ` in a topological space `X` connecting points `a` and `b` is continuous.
|
IsPathConnected.isConnected
theorem IsPathConnected.isConnected :
∀ {X : Type u_1} [inst : TopologicalSpace X] {F : Set X}, IsPathConnected F → IsConnected F
The theorem `IsPathConnected.isConnected` states that for any type `X` equipped with a topology and any set `F` of elements of type `X`, if `F` is a path-connected set, then it is also a connected set. Here, a set is path-connected if there exists a point within the set that can be connected to all other points in the set via a path entirely contained within the set. A connected set is a nonempty set where there is no non-trivial open partition, implying that the set cannot be separated into two nonempty open sets.
More concisely: If a path-connected subset of a topological space is nonempty, then it is also a connected subset.
|
IsPathConnected.joinedIn
theorem IsPathConnected.joinedIn :
∀ {X : Type u_1} [inst : TopologicalSpace X] {F : Set X}, IsPathConnected F → ∀ x ∈ F, ∀ y ∈ F, JoinedIn F x y := by
sorry
The theorem `IsPathConnected.joinedIn` states that for any topological space `X` and any subset `F` of `X`, if `F` is path-connected, then for any two points `x` and `y` in `F`, there exists a path within `F` that connects `x` and `y`. In the context of topology, a path between two points is essentially a continuous function from the unit interval into the topological space that starts at one point and ends at the other. In other words, if a set is path-connected, then any two points in the set can be joined by a path that stays entirely within the set.
More concisely: If `F` is a path-connected subset of a topological space `X`, then for any `x, y ∈ F`, there exists a path `p : I → F` with `p(0) = x` and `p(1) = y`.
|
IsPathConnected.image'
theorem IsPathConnected.image' :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {F : Set X},
IsPathConnected F → ∀ {f : X → Y}, ContinuousOn f F → IsPathConnected (f '' F)
The theorem `IsPathConnected.image'` states that if a function `f` is continuous on a set `F` and `F` is path-connected, then the image of `F` under `f` is also path-connected. In other words, if every two points in `F` can be connected by a path entirely within `F`, and `f` preserves the closeness of points, then every two points in `f(F)` can be connected by a path entirely within `f(F)`. This theorem can apply in the context of topological spaces, which are mathematical structures that allow the formal definition of concepts such as continuity, convergence, and closeness.
More concisely: If a continuous function maps a path-connected topological space to another topological space, then the image of the space is also path-connected.
|
Homeomorph.isPathConnected_preimage
theorem Homeomorph.isPathConnected_preimage :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set Y} (h : X ≃ₜ Y),
IsPathConnected (⇑h ⁻¹' s) ↔ IsPathConnected s
The theorem `Homeomorph.isPathConnected_preimage` states that for any topological spaces `X` and `Y`, and any homeomorphism `h` from `X` to `Y`, a set `s` in `Y` is path-connected if and only if its preimage under `h` in `X` is path-connected. In other words, a homeomorphism preserves the property of being path-connected between the original set and its image under the homeomorphism. A path-connected set, in this context, is defined as a set which contains at least one point that can be connected to all other points in the set via a path within the set.
More concisely: A homeomorphism preserves the path-connectedness of sets: if a set in a topological space is path-connected, then its preimage under a homeomorphism is also path-connected.
|
Path.continuous_uncurry_iff
theorem Path.continuous_uncurry_iff :
∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {Y : Type u_4} [inst_1 : TopologicalSpace Y]
{g : Y → Path x y}, Continuous ↿g ↔ Continuous g
This theorem states that for any topological spaces `X` and `Y`, and any points `x` and `y` in `X`, and any function `g` from `Y` to the set of paths from `x` to `y` in `X`, the function `g` is continuous if and only if the uncurried function `↿g` is continuous. Here, "uncurrying" a function refers to converting a function of multiple arguments into a function of one argument that returns another function, such that the original arguments can be provided one at a time.
More concisely: For any topological spaces X and Y, functions g : Y -> paths from x to y in X, and points x and y in X, the function g is continuous if and only if its uncurried version ↿g : Y x X -> path from x to y in X is continuous.
|
Path.source'
theorem Path.source' : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (self : Path x y), self.toFun 0 = x := by
sorry
This theorem states that the starting point of a `Path` in a topological space is equal to the initial point `x`. More specifically, when a `Path` from `x` to `y` in a topological space `X` is represented as a function `self.toFun`, the value of this function at `0` is `x`.
More concisely: In a topological space, the starting point of a path is equal to the path's initial point. In Lean 4 notation, if `p : Path X x y`, then `p 0 = x`.
|
Path.continuous_extend
theorem Path.continuous_extend :
∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), Continuous γ.extend
This theorem, `Path.continuous_extend`, states that for any given topological space `X` and any two points `x` and `y` in this space, if there is a path `γ` from `x` to `y`, then the extension of this path `γ` is continuous. In other words, you can extend the path without causing any discontinuities.
More concisely: If `X` is a topological space, `x` and `y` are points in `X`, and `γ` is a path from `x` to `y`, then the extension of `γ` is a continuous function from its domain to `X`.
|
Homeomorph.isPathConnected_image
theorem Homeomorph.isPathConnected_image :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y),
IsPathConnected (⇑h '' s) ↔ IsPathConnected s
The theorem `Homeomorph.isPathConnected_image` states that if `h` is a homeomorphism from type `X` to type `Y`, both equipped with a topological space structure, then the image of a set `s` under `h` is path-connected if and only if `s` is path-connected. In other words, a homeomorphism preserves the property of being path-connected: it maps path-connected sets to path-connected sets, and the pre-images of path-connected sets are also path-connected. This is true for all topological spaces `X` and `Y`, and any set `s` of elements of `X`.
More concisely: A homeomorphism preserves the path-connectedness of sets: if `h` is a homeomorphism from a topological space `X` to `Y` and `s` is a path-connected subset of `X`, then `h(s)` is a path-connected subset of `Y`, and vice versa.
|
IsPathConnected.image
theorem IsPathConnected.image :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {F : Set X},
IsPathConnected F → ∀ {f : X → Y}, Continuous f → IsPathConnected (f '' F)
The theorem `IsPathConnected.image` states that for any two topological spaces `X` and `Y`, if `F` is a path-connected subset of `X`, and `f` is a continuous function from `X` to `Y`, then the image of `F` under `f` (denoted by `f '' F`) is also path-connected. In other words, the continuous image of a path-connected set remains path-connected. This is a central concept in the study of topological spaces.
More concisely: If `F` is a path-connected subset of a topological space `X` and `f` is a continuous function from `X` to another topological space `Y`, then `f(F)` is a path-connected subset of `Y`.
|
Joined.symm
theorem Joined.symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Joined x y → Joined y x
The theorem `Joined.symm` states that for any topological space `X` and any two points `x` and `y` in `X`, if `x` and `y` are joined by a path (denoted as `Joined x y`), then `y` and `x` are also joined by a path (denoted as `Joined y x`). This property is also known as the symmetry of the relation "being joined by a path".
More concisely: For any topological space X and points x, y in X, if Joined x y then Joined y x.
|
Path.continuous
theorem Path.continuous : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), Continuous ⇑γ := by
sorry
This theorem states that for any given type `X` with a topology (`TopologicalSpace X`), and any two points `x` and `y` in `X`, if there exists a path (`γ`) from `x` to `y`, then the function mapping elements of the path (`γ`) to their images in `X` is continuous. In other words, the path from `x` to `y` can be traced without lifting the 'pen' from the 'paper', where 'pen' and 'paper' are metaphorical representations of the mathematical concepts of a function and a set respectively.
More concisely: Given a topological space `X` and points `x` and `y` with a continuous path `γ` between them, the function mapping `γ` to its image in `X` is continuous.
|
Continuous.path_extend
theorem Continuous.path_extend :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X}
{γ : Y → Path x y} {f : Y → ℝ}, Continuous ↿γ → Continuous f → Continuous fun t => (γ t).extend (f t)
This theorem, `Continuous.path_extend`, states that for any two types `X` and `Y` with topological space structures, and any two points `x` and `y` in `X`, if there is a function `γ : Y → Path x y` mapping from `Y` to paths between `x` and `y` and another function `f : Y → ℝ` mapping from `Y` to real numbers, such that both `γ` and `f` are continuous, then the function that takes a point `t` and extends the `t`-th path according to the `t`-th real number is also continuous. It's essentially saying that if you have a continuous way of picking paths and a continuous way of choosing extents, then combining these in a certain way gives you another continuous function.
More concisely: Given types `X` and `Y` with topological spaces, points `x, y ∈ X`, continuous functions `γ : Y → Path x y` and `f : Y → ℝ`, if for all `t ∈ Y`, the extended path `γ t (f t)` is a continuous function from `Y` to `Path x y`, then `γ` and `f` combine to form a continuous function `Y → Path x y`.
|
PathConnectedSpace.joined
theorem PathConnectedSpace.joined :
∀ {X : Type u_4} [inst : TopologicalSpace X] [self : PathConnectedSpace X] (x y : X), Joined x y
This theorem states that for any two points in a path-connected topological space, there exists a continuous path joining them. This implies that in a path-connected space, we can always find a path, that is continuous, between any pair of points. The relation "being joined by a path" is an equivalence relation, meaning that every point is joined to itself, if a point `x` is joined to a point `y`, then `y` is also joined to `x`, and if a point `x` is joined to a point `y` and `y` is joined to a point `z`, then `x` is joined to `z`.
More concisely: In a path-connected topological space, for any two points there exists a continuous path joining them.
|
Path.target
theorem Path.target : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), γ 1 = y
This theorem, "Path.target", states that for every path `γ` from point `x` to point `y` in any topological space `X`, the endpoint of the path (which is `γ` evaluated at `1`) is equal to `y`. The theorem holds for all types `X` and points `x` and `y` in `X`. In simpler terms, the theorem ensures that a path starting at `x` and ending at `y` indeed ends at `y`.
More concisely: For every path γ : X → ℝ with endpoints x and y in any topological space X, x = γ 1 implies y = γ 1.
|
Continuous.path_eval
theorem Continuous.path_eval :
∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {Y : Type u_4} [inst_1 : TopologicalSpace Y]
{f : Y → Path x y} {g : Y → ↑unitInterval}, Continuous f → Continuous g → Continuous fun y_1 => (f y_1) (g y_1)
The theorem `Continuous.path_eval` asserts that for any topological spaces `X` and `Y`, given two points `x` and `y` in `X`, a function `f` from `Y` to the set of paths from `x` to `y`, and a function `g` from `Y` to the unit interval `[0,1]` in ℝ, if both `f` and `g` are continuous, then the function that maps each element of `Y` to the point on the path `f(y_1)` at the parameter value `g(y_1)` is also continuous. This essentially states the continuity of path evaluation under certain conditions.
More concisely: Given continuous functions `f : Y → X → Path p x y` and `g : Y → [0, 1]` from a topological space `Y` to a path `p : X → X` between points `x` and `y` in a topological space `X`, the function `h : Y → X` defined by `h(y) = f(y)(g(y))` is continuous.
|
Path.extend_extends
theorem Path.extend_extends :
∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b) {t : ℝ} (ht : t ∈ Set.Icc 0 1),
γ.extend t = γ ⟨t, ht⟩
This theorem states that for all types `X`, assuming that `X` has a topology, and for any two points `a` and `b` in `X` with a path `γ` connecting them, if a real number `t` is in the closed interval [0, 1], then extending the path `γ` at `t` is equivalent to the path `γ` at `t`. In simpler terms, it states that the "extended" path at a point in the unit interval is the same as the original path at that point.
More concisely: For any connected topological space $(X, \tau)$, points $a, b \in X$ with a path $\gamma$ connecting them, and real number $t \in [0, 1]$, the extended path $\gamma \ast [t]$ is equal to $\gamma$ at point $t$, i.e., $\gamma \ast [t] = \gamma$.
|
JoinedIn.joined_subtype
theorem JoinedIn.joined_subtype :
∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {F : Set X} (h : JoinedIn F x y), Joined ⟨x, ⋯⟩ ⟨y, ⋯⟩ := by
sorry
The theorem `JoinedIn.joined_subtype` states that, for any topological space `X`, and any two points `x` and `y` in `X`, if `x` and `y` can be joined within a set `F` located in `X` (meaning there is a continuous path within `F` connecting `x` and `y`), then `x` and `y` can also be joined within the subtype `F` (implying that there is a path within the subset of `X` defined by `F` connecting `x` and `y`).
More concisely: If two points in a topological space can be joined by a continuous path within a subset, then they can be joined by a continuous path within the subtype.
|
Path.trans_pi_eq_pi_trans
theorem Path.trans_pi_eq_pi_trans :
∀ {ι : Type u_3} {χ : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (χ i)] {as bs cs : (i : ι) → χ i}
(γ₀ : (i : ι) → Path (as i) (bs i)) (γ₁ : (i : ι) → Path (bs i) (cs i)),
(Path.pi γ₀).trans (Path.pi γ₁) = Path.pi fun i => (γ₀ i).trans (γ₁ i)
The theorem `Path.trans_pi_eq_pi_trans` states that the composition of paths, when taken for a family of paths (each in some topological space `χ i`), is commutative with the operation of taking their pointwise product. In other words, given two families of paths `γ₀` and `γ₁` from `as` to `bs` and from `bs` to `cs` respectively, we can either first compose the paths within each family and then take their product, or first take the product of each family of paths and then compose, and the result will be the same.
More concisely: Given families of paths `γ₀:` χ i →bs → cs and `γ₁:` as →bs → cs in topological spaces, the commutativity of path composition and pointwise product holds: (γ₀ ∘ π i) ⊗ (γ₁) = (γ₀ ∧ π i) ⊗ (γ₁), where ∘ is composition, ∧ is the pointwise product, and ⊗ is the product of paths.
|
Path.trans_prod_eq_prod_trans
theorem Path.trans_prod_eq_prod_trans :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {a₁ a₂ a₃ : X}
{b₁ b₂ b₃ : Y} (γ₁ : Path a₁ a₂) (δ₁ : Path a₂ a₃) (γ₂ : Path b₁ b₂) (δ₂ : Path b₂ b₃),
(γ₁.prod γ₂).trans (δ₁.prod δ₂) = (γ₁.trans δ₁).prod (γ₂.trans δ₂)
This theorem states that path composition, in the context of topological spaces, commutes with taking products. Specifically, given topological spaces `X` and `Y`, points `a₁`, `a₂`, `a₃` in `X`, and points `b₁`, `b₂`, `b₃` in `Y`, and paths `γ₁` from `a₁` to `a₂`, `δ₁` from `a₂` to `a₃`, `γ₂` from `b₁` to `b₂`, and `δ₂` from `b₂` to `b₃`, the theorem asserts that the path obtained by first taking the product of `γ₁` and `γ₂` and then composing with the product of `δ₁` and `δ₂` is the same as the path obtained by first composing `γ₁` with `δ₁` and `γ₂` with `δ₂` and then taking the product.
More concisely: Given topological spaces `X` and `Y` and paths `γ₁ : X → X`, `δ₁ : X → X`, `γ₂ : Y → Y`, and `δ₂ : Y → Y`, the path compositions `(γ₁ ∘ δ₁) × (γ₂ ∘ δ₂)` and `(γ₁ × γ₂) ∘ (δ₁ × δ₂)` from `(a₁, b₁)` to `(a₃, b₃)` in `X × Y` are equal.
|
Path.symm_symm
theorem Path.symm_symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), γ.symm.symm = γ := by
sorry
The theorem `Path.symm_symm` states that for any topological space `X` and any two points `x` and `y` in `X`, if we take a path `γ` from `x` to `y`, and then take the reverse of the reverse of that path, we get back the original path `γ`. In other words, reversing a path twice gives us back the original path. This is true for any path in any topological space.
More concisely: For any topological space X and any two points x, y in X with a path γ between them, the reversed path of the reversed path γ is equal to γ.
|
Path.target'
theorem Path.target' : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (self : Path x y), self.toFun 1 = y := by
sorry
This theorem, `Path.target'`, states that for any topological space `X` and any two points `x` and `y` in `X`, the endpoint of a `Path` from `x` to `y` is `y`. In more detail, if you have a `Path` `self` that goes from `x` to `y`, then the function `toFun` applied to the endpoint `1` of the path (which ranges from `0` to `1`) will give you the point `y`.
More concisely: For any topological space X and any points x, y in X, the endpoint of a path from x to y is y. That is, the image of 1 under the function representing the path from x to y is equal to y.
|
IsPathConnected.preimage_coe
theorem IsPathConnected.preimage_coe :
∀ {X : Type u_1} [inst : TopologicalSpace X] {U W : Set X},
IsPathConnected W → W ⊆ U → IsPathConnected (Subtype.val ⁻¹' W)
This theorem states that if a set `W` is path-connected in a topological space `X`, then it remains path-connected when considered as a subset in a smaller ambient type `U`, provided that `U` contains `W`. Here, path-connected means that there is a point in the set that can be joined to all other points in the set. The function `Subtype.val ⁻¹' W` denotes the preimage of `W` under the function that extracts the underlying element from a subtype. This essentially means that we are considering `W` as a set in `U`, rather than in the larger space `X`.
More concisely: If a path-connected subset `W` of a topological space `X` is contained in a smaller space `U`, then `W` remains path-connected as a subset of `U`.
|
PathConnectedSpace.nonempty
theorem PathConnectedSpace.nonempty :
∀ {X : Type u_4} [inst : TopologicalSpace X] [self : PathConnectedSpace X], Nonempty X
This theorem states that for any given type `X`, if `X` is a topological space and also a path-connected space, then `X` is nonempty. In simpler terms, if there's a notion of "closeness" (topology) that allows us to trace a path from any point to any other point in `X` (path-connected), then there must be at least one point in `X`, i.e., `X` cannot be an empty set.
More concisely: If `X` is a non-empty, topological space that is also path-connected.
|
JoinedIn.mem
theorem JoinedIn.mem :
∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {F : Set X}, JoinedIn F x y → x ∈ F ∧ y ∈ F
This theorem states that for any topological space `X`, and any two points `x` and `y` of `X`, and a set `F` of `X`, if `x` and `y` are joined in `F` (i.e., there exists a path in `F` connecting `x` and `y`), then both `x` and `y` belong to the set `F`. In other words, the endpoints (`x` and `y`) of any path in `F` must themselves be elements of `F`.
More concisely: If `F` is a subset of a topological space `X`, and `x` and `y` are points in `X` with a path in `F` connecting them, then `x` and `y` are elements of `F`.
|
Path.extend.proof_1
theorem Path.extend.proof_1 : 0 ≤ 1
This theorem, `Path.extend.proof_1`, simply states that 0 is less than or equal to 1. In mathematical notation, this is expressed as \(0 \leq 1\). This is a fundamental and universal truth in the context of real numbers or integers.
More concisely: The theorem `Path.extend.proof_1` asserts that 0 is less than or equal to 1 (0 ≤ 1) in Lean 4.
|
Inducing.isPathConnected_iff
theorem Inducing.isPathConnected_iff :
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {F : Set X} {f : X → Y},
Inducing f → (IsPathConnected F ↔ IsPathConnected (f '' F))
The theorem `Inducing.isPathConnected_iff` states that for all topological spaces `X` and `Y`, and for a function `f` from `X` to `Y` that is inducing, a set `F` in `X` is path-connected if and only if the image of `F` under `f` is path-connected. Being path-connected means there is a point in the set that can be joined to all other points in the set. An inducing function is one that generates the same topology on the domain as the one on its range when restricted to the image of `f`.
More concisely: For an inducing function between topological spaces, a set is path-connected if and only if its image under the function is.
|
LocPathConnectedSpace.path_connected_basis
theorem LocPathConnectedSpace.path_connected_basis :
∀ {X : Type u_4} [inst : TopologicalSpace X] [self : LocPathConnectedSpace X] (x : X),
(nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsPathConnected s) id
This theorem states that for any topological space `X` that is locally path-connected, and any point `x` in `X`, the neighborhood filter of `x` has a basis consisting of path-connected neighborhoods. In other words, each neighborhood filter at a point in such a space can be generated from a collection of path-connected neighborhoods. Here, a neighborhood is path-connected if it contains a point that can be connected to all other points in the neighborhood via a path.
More concisely: In any locally path-connected topological space, each point has a neighborhood basis consisting of path-connected neighborhoods.
|
Path.source
theorem Path.source : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), γ 0 = x
This theorem states that for any given path `γ` between two points `x` and `y` in a topological space `X`, the source of the path (i.e., the point at which the path begins) is `x`. Specifically, when parameter `0` is given to the path `γ`, it returns the starting point `x`.
More concisely: For any path γ : X → X between points x and y in a topological space X, γ 0 = x.
|
pathConnectedSpace_iff_univ
theorem pathConnectedSpace_iff_univ :
∀ {X : Type u_1} [inst : TopologicalSpace X], PathConnectedSpace X ↔ IsPathConnected Set.univ
This theorem defines a condition for a topological space to be path connected. Specifically, it states that for any given type `X` with an instance of a topological space, `X` is a path-connected space if and only if the universal set of `X` is path-connected. In more mathematical terms, this means that a space is path-connected when there exists a continuous function that connects any two points in the space without leaving the space, and this condition is equivalent to the universal set (the set of all elements) being path-connected.
More concisely: A topological space `X` is path-connected if and only if its underlying set is path-connected.
|