op — Mathlib · SciLib

English

IsInvertedBy commutes with op and rightOp constructions in the presence of inversions.

Русский

IsInvertedBy сохраняется при операциях op и rightOp в условиях инвертирования.

LaTeX

$$$ W.IsInvertedBy L \Rightarrow W.rightOp.IsInvertedBy L.rightOp $$$

Lean4

theorem op {W : MorphismProperty C} {L : C ⥤ D} (h : W.IsInvertedBy L) : W.op.IsInvertedBy L.op := fun X Y f hf =>
  by
  haveI := h f.unop hf
  dsimp
  infer_instance

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