yonedaULiftEquiv_yonedaULift_map — Mathlib

English

A variant of map YonedaEquiv that uses the prime form to avoid type errors in certain situations.

Русский

Вариант map YonedaEquiv с примой, помогающий избежать ошибок типов в некоторых случаях.

LaTeX

$$$F.map\ g (J.yonedaEquiv' f) = f.val.app (Y) g.unop$$$

Lean4

theorem yonedaULiftEquiv_yonedaULift_map {X Y : C} (f : X ⟶ Y) :
    (yonedaULiftEquiv.{v'} J) (J.yonedaULift.map f) = ⟨f⟩ :=
  by
  rw [yonedaULiftEquiv_apply]
  simp [yonedaULift]

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