hasRightResolutions_iff_op — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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