uhpath01 — Mathlib

English

The homotopy class of the path from 0 to 1 in ULift I is represented by upath01.

Русский

Гомотопический класс пути от 0 к 1 в ULift I представлен upath01.

LaTeX

$$$$ uhpath01 = \\text{class of } upath01 \\text{ in } (\\text{TopCat}.f) \\Big(ULift (I)\\Big).$$$$

Lean4

/-- The homotopy path class of 0 → 1 in `ULift I` -/
def uhpath01 : @fromTop (TopCat.of <| ULift.{u} I) (ULift.up (0 : I)) ⟶ fromTop (ULift.up 1) :=
  ⟦upath01⟧

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