ιColimitType_eq_iff_of_isFiltered

English

If there exists an equivalence e: c.pt ≃ c'.pt and a coherence condition, then c'.IsColimit.

Русский

Если существует эквиваленция e: c.pt ≃ c'.pt и согласование, то c'.IsColimit.

LaTeX

$$c'.IsColimit$$

Lean4

theorem ιColimitType_eq_iff_of_isFiltered {j j' : J} (x : F.obj j) (y : F.obj j') :
    F.ιColimitType j x = F.ιColimitType j' y ↔ ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k), F.map f x = F.map f' y := by
  rw [ιColimitType_eq_iff, eqvGen_colimitTypeRel_iff_of_isFiltered]

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