isSStronglyConnected_iff — Mathlib

English

A quiver is IsSStronglyConnected if and only if for every pair of vertices i, j there exists a path from i to j of positive length.

Русский

Кьювер является IsSStronglyConnected тогда и только тогда, когда для любых вершин i, j существует путь i → j положительной длины.

LaTeX

$$$ IsSStronglyConnected(V) \\iff \\forall i,j:V, \\exists p:Path(i,j), 0 < \\text{length}(p) $$$

Lean4

@[simp]
theorem isSStronglyConnected_iff : IsSStronglyConnected V ↔ ∀ i j : V, ∃ p : Path i j, 0 < p.length :=
  Iff.rfl

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