mk_eq_mk_iff — Mathlib

English

Symmetry of left-homotopy: if f is left-homotopic to g, then g is left-homotopic to f.

Русский

Снова симметрия лево-гомотопии: если f лево-гомотопичен к g, то g лево-гомотопичен к f.

LaTeX

$$$ f \sim_L g \Rightarrow g \sim_L f$$$

Lean4

theorem mk_eq_mk_iff [ModelCategory C] [IsCofibrant X] (f g : X ⟶ Y) : mk f = mk g ↔ LeftHomotopyRel f g :=
  by
  rw [← (LeftHomotopyRel.equivalence X Y).eqvGen_iff]
  exact Quot.eq

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