toHomotopyConst — Mathlib

English

A path from x0 to x1 gives a homotopy between the constant maps at x0 and x1.

Русский

Путь от x0 к x1 задаёт гомотопию между константными отображениями в x0 и в x1.

LaTeX

$$$\text{toHomotopyConst} (p) : (\mathrm{ContinuousMap.const}\; Y\; x_0)\;\mathrm{Homotopy}\; (\mathrm{ContinuousMap.const}\; Y\; x_1)$$$

Lean4

/-- A path `Path x₀ x₁` generates a homotopy between constant functions `fun _ ↦ x₀` and
`fun _ ↦ x₁`. -/
@[simps!]
def toHomotopyConst (p : Path x₀ x₁) : (ContinuousMap.const Y x₀).Homotopy (ContinuousMap.const Y x₁)
    where
  toContinuousMap := p.toContinuousMap.comp ContinuousMap.fst
  map_zero_left _ := p.source
  map_one_left _ := p.target

Похожие утверждения