leftHomotopyClassEquivRightHomotopyClass_mk

English

For a morphism f: X → Y, the equivalence LH(X,Y) ≃ RH(X,Y) sends the representative mk(f) to mk(f).

Русский

Для морфизма f: X → Y эквиваленция LH(X,Y) ≃ RH(X,Y) отправляет представителя mk(f) в mk(f).

LaTeX

$$$\text{leftHomotopyClassEquivRightHomotopyClass}({\rm mk}(f)) = {\rm mk}(f)$$$

Lean4

@[simp]
theorem leftHomotopyClassEquivRightHomotopyClass_mk (f : X ⟶ Y) :
    leftHomotopyClassEquivRightHomotopyClass (.mk f) = .mk f :=
  rfl

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