nonempty_rightResolution_iff_op — Mathlib

English

For Φ, the right resolution at X₂ is nonempty iff the left resolution at Opposite(X₂) is nonempty.

Русский

Для Φ правое разрешение X₂ не пусто тогда и только тогда, когда не пусто левое разрешение Opposite(X₂).

LaTeX

$$$\operatorname{Nonempty}(\Phi.RightResolution(X_2)) \iff \operatorname{Nonempty}(\Phi.LeftResolution(\operatorname{Opposite}(X_2))).$$$

Lean4

theorem nonempty_rightResolution_iff_op (X₂ : C₂) :
    Nonempty (Φ.RightResolution X₂) ↔ Nonempty (Φ.op.LeftResolution (Opposite.op X₂)) :=
  Equiv.nonempty_congr
    { toFun := fun R => R.op
      invFun := fun L => L.unop }

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