multiequalizerEquiv_apply — Mathlib

English

Continuation of auxiliary lemmas ensuring compatibility with the multicospan maps.

Русский

Продолжение вспомогательных лемм, обеспечивающих совместимость с отображениями мультикоспана.

LaTeX

$$$\\text{Aux proof 2 for } multiequalizerEquivAux$$$

Lean4

@[simp]
theorem multiequalizerEquiv_apply {J : MulticospanShape.{w, w'}} (I : MulticospanIndex J C) [HasMultiequalizer I]
    [PreservesLimit I.multicospan (forget C)] (x : ToType (multiequalizer I)) (i : J.L) :
    ((Concrete.multiequalizerEquiv I) x : ∀ i : J.L, ToType (I.left i)) i = Multiequalizer.ι I i x :=
  rfl

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