of_equiv — Mathlib

English

If there is an equivalence e: c.pt ≃ c'.pt that respects each injection, then c' is also a colimit cocone.

Русский

Если существует эквивалентность e: c.pt ≃ c'.pt, сохраняющая все инъекции, то c' тоже является коллимитным коконом.

LaTeX

$$$\text{of_equiv } {c' : CoconeTypes.{w_2} F} (e : c.pt \simeq c'.pt) (he : \forall j x, c'.ι j x = e (c.ι j x)) : c'.IsColimit$$$

Lean4

theorem of_equiv {c' : CoconeTypes.{w₂} F} (e : c.pt ≃ c'.pt) (he : ∀ j x, c'.ι j x = e (c.ι j x)) : c'.IsColimit where
  bijective := by
    convert Function.Bijective.comp e.bijective hc.bijective
    ext y
    obtain ⟨j, x, rfl⟩ := F.ιColimitType_jointly_surjective y
    simp_all

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