SimplyConnectedSpace.paths_homotopic
theorem SimplyConnectedSpace.paths_homotopic :
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : SimplyConnectedSpace X] {x y : X} (p₁ p₂ : Path x y),
p₁.Homotopic p₂
This theorem states that in a simply connected topological space, any two paths between the same two points are homotopic. In other words, given a topological space 'X' that is simply connected and two points 'x' and 'y' in 'X', for any two paths 'p₁' and 'p₂' from 'x' to 'y', there exists a continuous transformation from 'p₁' to 'p₂', which is what it means for the paths to be homotopic.
More concisely: In a simply connected topological space, any two paths between the same two points are homotopic.
|
simply_connected_iff_paths_homotopic
theorem simply_connected_iff_paths_homotopic :
∀ {Y : Type u_1} [inst : TopologicalSpace Y],
SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
A topological space is simply connected if and only if it is path connected, and for any two points in the space, there is at most one path between them up to homotopy. In other words, any two paths between the same two points can be continuously deformed into each other. Here, 'PathConnectedSpace Y' indicates that for any two points in the space 'Y', there exists a continuous path connecting them, and 'Subsingleton (Path.Homotopic.Quotient x y)' indicates that the quotient space of homotopic paths between points 'x' and 'y' contains at most one element, meaning all paths between 'x' and 'y' are homotopic.
More concisely: A topological space is simply connected if and only if it is path connected and any two paths between the same two points are homotopic.
|
simply_connected_iff_paths_homotopic'
theorem simply_connected_iff_paths_homotopic' :
∀ {Y : Type u_1} [inst : TopologicalSpace Y],
SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), p₁.Homotopic p₂
This theorem, `simply_connected_iff_paths_homotopic'`, states that for any type `Y` equipped with a topological space structure, `Y` is simply connected if and only if it is path-connected and for any two points `x` and `y` in `Y`, any two paths from `x` to `y`, say `p₁` and `p₂`, are homotopic. In simpler terms, a space is simply connected when it is path-connected (there exists a path between any two points) and any two paths between the same pair of points can be continuously transformed into each other.
More concisely: A topological space `Y` is simply connected if and only if it is path-connected and any two paths between any pair of points in `Y` are homotopic.
|