refl — Mathlib

English

The constant path from a point to itself assigns every t to that point.

Русский

Путь, константный между точками, отправляет каждое t в эту же точку.

LaTeX

$$$ (\\text{refl}(x)) : I \\to X \\text{ satisfies } (\\text{refl}(x))(t)=x \\text{ for all } t. $$$

Lean4

/-- The constant path from a point to itself -/
@[refl, simps!]
def refl (x : X) : Path x x where
  toContinuousMap := .const I x
  source' := rfl
  target' := rfl

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