refl — Mathlib

English

For any path p, there exists a homotopy from p to p given by the constant in time map, i.e., F(t, x) = p(x).

Русский

Для любого пути p существует гомотопия от p к самому себе, задаваемая константой по времени: F(t, x) = p(x).

LaTeX

$$$\forall p : Path\, x_0 x_1, \; \exists F : p.Homotopy p, \forall (t,x) \in I \times I,\; F(t,x) = p(x)$$$

Lean4

/-- Given a path `p`, we can define a `Homotopy p p` by `F (t, x) = p x`.
-/
@[simps!]
def refl (p : Path x₀ x₁) : Homotopy p p :=
  ContinuousMap.HomotopyRel.refl p.toContinuousMap {0, 1}

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