guitartExact_iff_isConnected_downwards

English

Guitart exactness of w is equivalent to: for all g, IsConnected (w.CostructuredArrowDownwards g).

Русский

Точность Гитхарта эквивалентна тому, что для каждого g связность снизу.

LaTeX

$$$w.GuitartExact \iff \forall g, \operatorname{IsConnected}\big(w.CostructuredArrowDownwards g\big)$$$

Lean4

theorem guitartExact_iff_isConnected_downwards :
    w.GuitartExact ↔ ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (w.CostructuredArrowDownwards g) := by
  simp only [guitartExact_iff_isConnected_rightwards, isConnected_rightwards_iff_downwards]

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