ContinuousMap.homotopic_const_iff
theorem ContinuousMap.homotopic_const_iff :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x₀ x₁ : X}
[inst_2 : Nonempty Y], (ContinuousMap.const Y x₀).Homotopic (ContinuousMap.const Y x₁) ↔ Joined x₀ x₁
The theorem `ContinuousMap.homotopic_const_iff` states that for any two points `x₀` and `x₁` in a topological space `X`, and for any non-empty topological space `Y`, two constant continuous maps from `X` to `Y` with values `x₀` and `x₁` are homotopic if and only if `x₀` and `x₁` are joined by a path in the space `Y`. Here, "being joined by a path" is defined as the existence of a continuous function (a "path") from the interval [0,1] into `Y` which starts at `x₀` and ends at `x₁`.
More concisely: Two constant continuous maps from a topological space to another non-empty topological space with different values are homotopic if and only if the values represent connected points in the target space through a path.
|
Path.Homotopic.map_lift
theorem Path.Homotopic.map_lift :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x₀ x₁ : X} (P₀ : Path x₀ x₁)
(f : C(X, Y)), ⟦P₀.map ⋯⟧ = Path.Homotopic.Quotient.mapFn ⟦P₀⟧ f
The theorem `Path.Homotopic.map_lift` states that for any two points `x₀` and `x₁` in a topological space `X`, any path `P₀` from `x₀` to `x₁`, and any continuous function `f` from `X` to another topological space `Y`, the homotopy class (equivalence class of paths under homotopy) of the image of `P₀` under `f` is equal to the image of the homotopy class of `P₀` under `f`. In more mathematical terms, it asserts that the function `Path.Homotopic.Quotient.mapFn` is well-defined on homotopy classes of paths, meaning that the result of first mapping a path and then taking the homotopy class is the same as first taking the homotopy class and then mapping.
More concisely: The homotopy class of a path in a topological space under a continuous function is equal to the image of its homotopy class under that function.
|