iff_of_iso — Mathlib

English

If F1 and F2 are isomorphic, W is inverted by F1 iff inverted by F2.

Русский

Если F1 и F2 изоморфны, то W разворачивается по F1 тогда и только тогда по F2.

LaTeX

$$$ W.IsInvertedBy F_1 \iff W.IsInvertedBy F_2 \text{ for } F_1 \cong F_2 $$$

Lean4

theorem iff_of_iso (W : MorphismProperty C) {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂) : W.IsInvertedBy F₁ ↔ W.IsInvertedBy F₂ :=
  by
  dsimp [IsInvertedBy]
  simp only [NatIso.isIso_map_iff e]

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