exists_good_pathObject — Mathlib

English

If f and g are right-homotopic, then there exists a path object P for Y such that P is good and P.RightHomotopy f g is nonempty.

Русский

Если f и g правой гомотопии эквивалентны, тогда существует путь-объект P для Y такой, что P является хорошим и P.RightHomotopy f g непусто.

LaTeX

$$$\\exists P : PathObject Y,\\; P.IsGood \\wedge Nonempty (P.RightHomotopy f g)$$$

Lean4

theorem exists_good_pathObject [ModelCategory C] {f g : X ⟶ Y} (h : RightHomotopyRel f g) :
    ∃ (P : PathObject Y), P.IsGood ∧ Nonempty (P.RightHomotopy f g) :=
  by
  obtain ⟨P, ⟨h⟩⟩ := h
  exact h.exists_good_pathObject

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