guitartExact_iff_isConnected_rightwards

English

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

Русский

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

LaTeX

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

Lean4

theorem guitartExact_iff_isConnected_rightwards :
    w.GuitartExact ↔ ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (w.StructuredArrowRightwards g) :=
  ⟨fun h => h.isConnected_rightwards, fun h => ⟨h⟩⟩

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