nonempty_leftResolution_iff_op — Mathlib

English

For Φ, the left resolution at X₂ is nonempty iff the opposite right resolution at X₂^{op} is nonempty.

Русский

Для Φ левого разрешения при X₂ существует не пустое разрешение тогда и только тогда, когда противоположное правое разрешение X₂^{op} не пусто.

LaTeX

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

Lean4

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

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