leftHomotopyClassEquivRightHomotopyClass_symm_mk

English

The inverse of the left→right equivalence, applied to mk(f), returns mk(f).

Русский

Обратное к преобразованию лево-право, применённое к mk(f), возвращает mk(f).

LaTeX

$$$\left(\mathrm{leftHomotopyClassEquivRightHomotopyClass}.\mathrm{symm}\right)({\rm mk}(f)) = {\rm mk}(f)$$$

Lean4

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

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