guitartExact_iff_initial — Mathlib

English

Guitart exactness is equivalent to the initiality condition: for all X2, the downward structured arrow is initial.

Русский

Точность Гитхарта эквивалентна начальному условию: для всех X2 структура стрелка вниз инициальна.

LaTeX

$$$\mathrm{GuitartExact} \iff \forall X_2, (\mathrm{structuredArrowDownwards}\, X_2).\mathrm{Initial}$$$

Lean4

theorem guitartExact_iff_initial : w.GuitartExact ↔ ∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial :=
  ⟨fun _ _ => ⟨fun _ => inferInstance⟩,
    by
    rw [guitartExact_iff_isConnected_downwards]
    intros
    infer_instance⟩

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