op_isoClosure — Mathlib

English

The operation of taking opposites commutes with isoClosure: P.isoClosure.op = P.op.isoClosure.

Русский

Операция взятия противоположной композиции с изоморфизмами коммутирует: P.isoClosure.op = P.op.isoClosure.

LaTeX

$$$P.isoClosure^{\mathrm{op}} = P^{\mathrm{op}}.\mathrm{isoClosure}$$$

Lean4

theorem op_isoClosure (P : ObjectProperty C) : P.isoClosure.op = P.op.isoClosure :=
  by
  ext ⟨X⟩
  exact ⟨fun ⟨Y, h, ⟨e⟩⟩ ↦ ⟨op Y, h, ⟨e.op.symm⟩⟩, fun ⟨Y, h, ⟨e⟩⟩ ↦ ⟨Y.unop, h, ⟨e.unop.symm⟩⟩⟩

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