hasLeftResolutions_iff_op — Mathlib

English

Φ.HasLeftResolutions holds iff Φ.op.HasRightResolutions holds.

Русский

Условия HasLeftResolutions для Φ эквивалентны HasRightResolutions для Φ.op.

LaTeX

$$$\text{HasLeftResolutions}(\Phi) \iff \text{HasRightResolutions}(\Phi^{op}).$$$

Lean4

theorem hasLeftResolutions_iff_op : Φ.HasLeftResolutions ↔ Φ.op.HasRightResolutions :=
  ⟨fun _ X₂ => ⟨(Classical.arbitrary (Φ.LeftResolution X₂.unop)).op⟩, fun _ X₂ =>
    ⟨(Classical.arbitrary (Φ.op.RightResolution (Opposite.op X₂))).unop⟩⟩

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