pos_cycle — Mathlib

English

For any IsSStronglyConnected V and any vertex v, there exists a path from v to itself of positive length.

Русский

Для любого IsSStronglyConnected V и любой вершины v существует путь v → v положительной длины.

LaTeX

$$$ \\forall V [Quiver V], IsSStronglyConnected V \\rightarrow \\forall v:\\ V, \\exists p:\\text{Path}(v,v), 0 < p.length $$$

Lean4

theorem pos_cycle (h : IsSStronglyConnected V) (v : V) : ∃ p : Path v v, 0 < p.length :=
  h v v

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