op_map — Mathlib

English

For φ : W.LeftFraction X Y, mapping and then taking op equals taking op first and then mapping with L.op.

Русский

Для φ : W.LeftFraction X Y отображение и затем взятие противоположного эквивалентно взятию противоположного сначала и затем отображению через L.op.

LaTeX

$$$\forall {C} {D} [\text{Category } C] [\text{Category } D] (φ : W.LeftFraction X Y) (L : C \to D) (hL : W.IsInvertedBy L), (φ.map L hL).op = φ.op.map L.op hL.op$$$

Lean4

theorem op_map {X Y : C} (φ : W.LeftFraction X Y) (L : C ⥤ D) (hL : W.IsInvertedBy L) :
    (φ.map L hL).op = φ.op.map L.op hL.op :=
  by
  dsimp [map, RightFraction.map]
  rw [op_inv]

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