eq — Mathlib · SciLib

English

If the StronglyConnectedComponent of a equals that of b, then there is a path from a to b and a path from b to a.

Русский

Если компонент сильной связности a равен компоненту сильной связности b, то существуют пути a → b и b → a.

LaTeX

$$$ (a,b:\\ V),\\; (a:\\text{StronglyConnectedComponent }V) = b \\Rightarrow (\\text{Nonempty}(\\text{Path}(a,b)) \\wedge \\text{Nonempty}(\\text{Path}(b,a))) $$$

Lean4

protected theorem eq (a b : V) : (a : StronglyConnectedComponent V) = b ↔ (Nonempty (Path a b) ∧ Nonempty (Path b a)) :=
  Quotient.eq''

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