ContinuousMap.HomotopyWith.prop
theorem ContinuousMap.HomotopyWith.prop :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
{P : C(X, Y) → Prop} (F : f₀.HomotopyWith f₁ P) (t : ↑unitInterval), P (F.curry t)
This theorem states that for any topological spaces `X` and `Y`, and any continuous maps `f₀` and `f₁` from `X` to `Y`, given a property `P` that applies to continuous maps from `X` to `Y`, if there exists a homotopy `F` between `f₀` and `f₁` that satisfies `P`, then for every point `t` in the unit interval `[0,1]`, the continuous map obtained by currying the homotopy `F` at point `t` also satisfies the property `P`.
More concisely: Given continuous maps `f₀`, `f₁` : X -> Y between topological spaces `X` and `Y`, a homotopy `F` : X x [0,1] -> Y between `f₀` and `f₁`, and a property `P` that preserves composition with continuous functions, if `F` satisfies `P`, then for all `t` in [0,1], the map `x => F(x, t)` satisfies `P`.
|
ContinuousMap.HomotopyWith.prop'
theorem ContinuousMap.HomotopyWith.prop' :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
{P : C(X, Y) → Prop} (self : f₀.HomotopyWith f₁ P) (t : ↑unitInterval),
P { toFun := fun x => self.toFun (t, x), continuous_toFun := ⋯ }
This theorem states that for any two continuous functions `f₀` and `f₁` from topological space `X` to topological space `Y`, and any property `P` of continuous functions from `X` to `Y`, if there exists a homotopy between `f₀` and `f₁` that satisfies `P`, then for each `t` in the unit interval `[0,1]`, the intermediate map at `t`, derived from the homotopy, also satisfies the property `P`. Here, a homotopy is a continuous deformation from `f₀` to `f₁` where each intermediate state is also a continuous function.
More concisely: If `f₀` and `f₁` are continuous functions from a topological space `X` to another topological space `Y`, and there exists a homotopy between them such that each intermediate map satisfies property `P`, then every intermediate map at `t` in the unit interval also satisfies property `P`.
|
ContinuousMap.Homotopy.apply_one
theorem ContinuousMap.Homotopy.apply_one :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
(F : f₀.Homotopy f₁) (x : X), F (1, x) = f₁ x
This theorem states that for any two continuous maps `f₀` and `f₁` from a topological space `X` to another topological space `Y`, and any homotopy `F` between `f₀` and `f₁`, the value of `F` at `(1, x)` is equal to the value of `f₁` at `x` for any `x` in `X`. In other words, at the end of the homotopy (when the first parameter is 1), the homotopy function `F` becomes the target function `f₁`. This is connected to the concept of homotopy in topology, where a homotopy is a continuous transformation from one function to another.
More concisely: For any continuous functions `f₀` and `f₁` from a topological space `X` to a topological space `Y` with a homotopy `F` between them, `F (1, x) = f₁ (x)` for all `x` in `X`.
|
ContinuousMap.Homotopy.apply_zero
theorem ContinuousMap.Homotopy.apply_zero :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
(F : f₀.Homotopy f₁) (x : X), F (0, x) = f₀ x
This theorem states that for any two continuous maps `f₀` and `f₁` from a topological space `X` to another topological space `Y`, and any homotopy `F` between `f₀` and `f₁`, the value of `F` at `(0, x)` is equal to the value of `f₀` at `x` for any `x` in `X`. In other words, at the start of the homotopy (when the homotopy parameter is 0), `F` coincides with the initial map `f₀`.
More concisely: Given continuous maps `f₀` and `f₁` from a topological space `X` to a topological space `Y`, and a homotopy `F` between them, for all `x` in `X`, `F 0 x = f₀ x`.
|
ContinuousMap.Homotopic.piMap
theorem ContinuousMap.Homotopic.piMap :
∀ {ι : Type u_2} {X : ι → Type u_3} {Y : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)]
[inst_1 : (i : ι) → TopologicalSpace (Y i)] {f₀ f₁ : (i : ι) → C(X i, Y i)},
(∀ (i : ι), (f₀ i).Homotopic (f₁ i)) → (ContinuousMap.piMap f₀).Homotopic (ContinuousMap.piMap f₁)
The theorem `ContinuousMap.Homotopic.piMap` states that for any type `ι`, and families of types `X` and `Y` indexed by `ι`, where each `X i` and `Y i` are endowed with a topological space structure, if we have two families of continuous maps `f₀` and `f₁` from `X i` to `Y i` for each `i : ι` such that each `f₀ i` is homotopic to `f₁ i`, then the combined continuous maps `ContinuousMap.piMap f₀` and `ContinuousMap.piMap f₁` (which are formed by collecting all the maps `f₀ i` and `f₁ i` respectively) are also homotopic. In other words, it's suggesting that homotopy is preserved under the operation of combining continuous maps.
More concisely: Given types `ι`, families of topological spaces `(X : ��ype i => Type)` and `(Y : ��ype i => Type)`, and families of continuous maps `(f₀ : ∀ i, X i → Y i)` and `(f₁ : ∀ i, X i → Y i)` with each `f₀ i` homotopic to `f₁ i`, the corresponding combined maps `ContinuousMap.piMap f₀` and `ContinuousMap.piMap f₁` are homotopic.
|
ContinuousMap.Homotopic.pi
theorem ContinuousMap.Homotopic.pi :
∀ {X : Type u} {ι : Type u_2} [inst : TopologicalSpace X] {Y : ι → Type u_3}
[inst_1 : (i : ι) → TopologicalSpace (Y i)] {f₀ f₁ : (i : ι) → C(X, Y i)},
(∀ (i : ι), (f₀ i).Homotopic (f₁ i)) → (ContinuousMap.pi f₀).Homotopic (ContinuousMap.pi f₁)
The theorem `ContinuousMap.Homotopic.pi` states that if, for every index `i` of a certain type `ι`, two continuous maps from a topological space `X` to topological spaces `Y i` (which may vary with `i`) are homotopic, then the product of the maps formed from the first set, `f₀`, is homotopic to the product of the maps formed from the second set, `f₁`. Here, "homotopic" means that there is a continuous deformation between the two maps, preserving their domain and codomain. In other words, if each map from `X` to `Y i` in the first collection is continuously deformable into the corresponding map in the second collection, then the same holds for the product maps.
More concisely: If for every index `i`, continuous maps `f₀ i` and `f₁ i` from a topological space `X` to `Y i` are homotopic, then the product maps `∏i f₀ i` and `∏i f₁ i` from `X` to `∏i Y i` are homotopic.
|
ContinuousMap.HomotopyLike.map_zero_left
theorem ContinuousMap.HomotopyLike.map_zero_left :
∀ {X : outParam (Type u_3)} {Y : outParam (Type u_4)} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{F : Type u_5} {f₀ f₁ : outParam C(X, Y)} [inst_2 : FunLike F (↑unitInterval × X) Y]
[self : ContinuousMap.HomotopyLike F f₀ f₁] (f : F) (x : X), f (0, x) = f₀ x
This theorem is named `ContinuousMap.HomotopyLike.map_zero_left` and it states that for any topological spaces `X` and `Y`, any two continuous maps `f₀` and `f₁` from `X` to `Y`, and any homotopy `f` between `f₀` and `f₁` (which is represented as a function-like object of type `F` mapping from the Cartesian product of the unit interval and `X` to `Y`), the value of the homotopy `f` at `(0, x)` for any point `x` in `X` is equal to the value of the initial function `f₀` at `x`. In other words, the homotopy starts from the initial function `f₀` at the beginning of the unit interval (at 0).
More concisely: For any continuous maps `f₀`, `f₁` and homotopy `F` between them from `X` to `Y`, `F (0, x) = f₀ x` for all `x` in `X`.
|
ContinuousMap.Homotopic.refl
theorem ContinuousMap.Homotopic.refl :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y)),
f.Homotopic f
This theorem states that for any continuous map `f` from a topological space `X` to another topological space `Y`, the map `f` is homotopic to itself. In other words, there exists a continuous transformation (or homotopy) from the function `f` to itself within the same topological spaces. This is an application of the reflexive property of homotopy in continuous mapping.
More concisely: Every continuous function from a topological space to itself is homotopic to itself.
|
ContinuousMap.HomotopyLike.map_one_left
theorem ContinuousMap.HomotopyLike.map_one_left :
∀ {X : outParam (Type u_3)} {Y : outParam (Type u_4)} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
{F : Type u_5} {f₀ f₁ : outParam C(X, Y)} [inst_2 : FunLike F (↑unitInterval × X) Y]
[self : ContinuousMap.HomotopyLike F f₀ f₁] (f : F) (x : X), f (1, x) = f₁ x
The theorem `ContinuousMap.HomotopyLike.map_one_left` states that for any two continuous functions `f₀` and `f₁` from a topological space `X` to another topological space `Y`, and for any homotopy `f` between them (represented by a function `F` that takes a pair consisting of a real number in the unit interval `[0,1]` and a point in `X` and returns a point in `Y`), the value of the homotopy at `(1, x)` for any `x` in `X` is equal to the value of the function `f₁` at `x`. This essentially means that at the endpoint of our unit interval, the homotopy `f` should coincide with the function `f₁`.
More concisely: For any continuous functions `f₀` and `f₁` from a topological space `X` to `Y` with a homotopy `F` between them, `F (1, x) = f₁ (x)` for all `x` in `X`.
|
ContinuousMap.Homotopy.continuous
theorem ContinuousMap.Homotopy.continuous :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
(F : f₀.Homotopy f₁), Continuous ⇑F
This theorem, which has been deprecated in favor of `map_continuous`, states that for any two continuous functions `f₀` and `f₁` from a topological space `X` to another topological space `Y`, if there exists a homotopy `F` between `f₀` and `f₁`, then the function `F` is continuous. Here, `f₀.Homotopy f₁` means `F` is a continuous transformation from function `f₀` to function `f₁`. The theorem holds for all types `X` and `Y` that have a topology defined on them.
More concisely: If two continuous functions between topological spaces have a homotopy between them, then the homotopy is a continuous function.
|
ContinuousMap.Homotopy.map_zero_left
theorem ContinuousMap.Homotopy.map_zero_left :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
(self : f₀.Homotopy f₁) (x : X), self.toFun (0, x) = f₀ x
This theorem states that for any two continuous functions `f₀` and `f₁` from a topological space `X` to another topological space `Y`, a homotopy `self` between `f₀` and `f₁` has the property that the value of the map of `self` at `(0, x)` for any `x` in `X` is equal to the value of `f₀` at `x`. In other words, at the "start" of the homotopy (where the first parameter is 0), the homotopy function is equivalent to the initial function `f₀`.
More concisely: Given continuous functions `f₀` and `f₁` from a topological space `X` to a topological space `Y` and a homotopy `self` between them, for all `x` in `X`, `self 0 x = f₀ x`.
|
ContinuousMap.Homotopy.map_one_left
theorem ContinuousMap.Homotopy.map_one_left :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
(self : f₀.Homotopy f₁) (x : X), self.toFun (1, x) = f₁ x
This theorem, named `ContinuousMap.Homotopy.map_one_left`, states that for any two continuous maps `f₀` and `f₁` between topological spaces `X` and `Y`, and a homotopy `self` from `f₀` to `f₁`, the value of the homotopy at `(1, x)` is equal to the value of `f₁` at `x` for any `x` in `X`. This essentially means that the homotopy at 1 is equal to the end function `f₁`.
More concisely: For any continuous maps `f₀`, `f₁` and homotopy `self` between them, `self 1 x = f₁ x` for all `x` in the domain of the maps.
|
ContinuousMap.Homotopic.hcomp
theorem ContinuousMap.Homotopic.hcomp :
∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
[inst_2 : TopologicalSpace Z] {f₀ f₁ : C(X, Y)} {g₀ g₁ : C(Y, Z)},
f₀.Homotopic f₁ → g₀.Homotopic g₁ → (g₀.comp f₀).Homotopic (g₁.comp f₁)
This theorem states that given two pairs of homotopic continuous maps, specifically `f₀` and `f₁` from a topological space `X` to a topological space `Y`, and `g₀` and `g₁` from `Y` to another topological space `Z`, if both pairs are homotopic, then the compositions of the maps (i.e., `g₀` composed with `f₀` and `g₁` composed with `f₁`) are also homotopic. In mathematical terms, if `f₀` is homotopic to `f₁` and `g₀` is homotopic to `g₁`, then `g₀ ∘ f₀` is homotopic to `g₁ ∘ f₁`.
More concisely: Given continuous maps `f₀`, `f₁` from X to Y and `g₀`, `g₁` from Y to Z, if `f₀` is homotopic to `f₁` and `g₀` is homotopic to `g₁`, then `g₀ ∘ f₀` is homotopic to `g₁ ∘ f₁`.
|
ContinuousMap.HomotopyRel.eq_fst
theorem ContinuousMap.HomotopyRel.eq_fst :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)} {S : Set X}
(F : f₀.HomotopyRel f₁ S) (t : ↑unitInterval) {x : X}, x ∈ S → F (t, x) = f₀ x
This theorem, `ContinuousMap.HomotopyRel.eq_fst`, states that for any topological spaces `X` and `Y`, given continuous maps `f₀` and `f₁` from `X` to `Y`, a subset `S` of `X`, and a homotopy `F` between `f₀` and `f₁` that is fixed on `S`, then for any `x` in `S` and any `t` in the unit interval `[0,1]`, the value of the homotopy `F` at `(t, x)` equals the value of the initial function `f₀` at `x`. Thus, the homotopy `F` starts at `f₀` for all points in the set `S`.
More concisely: For any continuous maps `f₀`, `f₁` from a topological space `X` to another space `Y`, a subset `S` of `X`, and a homotopy `F` between `f₀` and `f₁` fixed on `S`, the value of `F` at `(t, x)` equals the value of `f₀` at `x` for all `x` in `S` and `t` in [0,1].
|
ContinuousMap.HomotopyWith.ext
theorem ContinuousMap.HomotopyWith.ext :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
{P : C(X, Y) → Prop} {F G : f₀.HomotopyWith f₁ P}, (∀ (x : ↑unitInterval × X), F x = G x) → F = G
This theorem states that for any two topological spaces `X` and `Y`, and any two continuous functions `f₀` and `f₁` from `X` to `Y`, if `P` is a property of the continuous functions, and `F` and `G` are both homotopies from `f₀` to `f₁` satisfying the property `P`, then if `F` and `G` agree on all points in the product of the unit interval `[0,1]` and `X`, then `F` and `G` are the same. In other words, two homotopies satisfying a certain property are equal if they coincide on the unit interval cross the topological space.
More concisely: Given topological spaces X and Y, continuous functions f₀, f₁ : X → Y, property P for continuous functions, and homotopies F, G : [0, 1] × X → Y satisfying P(F), P(G) and F = G on [0, 1] × X, then F = G.
|
ContinuousMap.Homotopic.trans
theorem ContinuousMap.Homotopic.trans :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] ⦃f g h : C(X, Y)⦄,
f.Homotopic g → g.Homotopic h → f.Homotopic h
The theorem `ContinuousMap.Homotopic.trans` states that, for any topological spaces `X` and `Y`, if there exists a homotopy between two continuous maps `f` and `g` from `X` to `Y`, and there exists a homotopy between `g` and another continuous map `h` from `X` to `Y`, then there also exists a homotopy between `f` and `h`. This establishes transitivity for the relation of being homotopic in the context of continuous maps between topological spaces.
More concisely: If two continuous maps between topological spaces are homotopic to each other, and each is homotopic to a third map, then the first two maps are homotopic to each other through the third map.
|
ContinuousMap.Homotopy.congr_fun
theorem ContinuousMap.Homotopy.congr_fun :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
{F G : f₀.Homotopy f₁}, F = G → ∀ (x : ↑unitInterval × X), F x = G x
This theorem, `ContinuousMap.Homotopy.congr_fun`, states that for any type `X` with a topology, and any type `Y` also with a topology, given two continuous maps `f₀` and `f₁` from `X` to `Y`, and two homotopies `F` and `G` from `f₀` to `f₁`, if `F` and `G` are the same, then for any pair consisting of a real number in the unit interval `[0,1]` and an element of `X`, the value of `F` at this pair is equal to the value of `G` at this pair. In other words, two equal homotopies between two continuous functions agree on all points in the unit interval cross the domain space.
More concisely: If `f₀` and `f₁` are continuous maps from a topological space `X` to another topological space `Y`, and `F` and `G` are homotopies from `f₀` to `f₁`, then for all `x ∈ X` and `t ∈ [0,1]`, `F t x = G t x`.
|
ContinuousMap.HomotopicRel.homotopic
theorem ContinuousMap.HomotopicRel.homotopic :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {S : Set X} {f₀ f₁ : C(X, Y)},
f₀.HomotopicRel f₁ S → f₀.Homotopic f₁
This theorem states that for any two types `X` and `Y` equipped with topological spaces, any set `S` of `X`, and any two continuous maps `f₀` and `f₁` from `X` to `Y`, if `f₀` and `f₁` are homotopic relative to the set `S`, then `f₀` and `f₁` are homotopic. In the context of topology, "homotopic" means there exists a continuous deformation from one function to the other while "homotopic relative to a set" means the deformation is such that points in the set `S` are always mapped to the same points.
More concisely: If `X` and `Y` are topological spaces, `S ⊆ X` is a set, and `f₀` and `f₁` are continuous maps from `X` to `Y` that are homotopic relative to `S`, then `f₀` and `f₁` are homotopic.
|