exists_path_of_stronglyConnectedComponent_eq

English

If mk a equals mk b in StronglyConnectedComponent, then there exist paths both from a to b and from b to a.

Русский

Если mk a = mk b в StronglyConnectedComponent, тогда существуют пути a → b и b → a.

LaTeX

$$$ (\\text{StronglyConnectedComponent.mk } a) = (\\text{StronglyConnectedComponent.mk } b) \\Rightarrow \\text{Nonempty}(\\text{Path}(a,b)) \\wedge \\text{Nonempty}(\\text{Path}(b,a)) $$$

Lean4

theorem exists_path_of_stronglyConnectedComponent_eq {a b : V} (h : (a : StronglyConnectedComponent V) = b) :
    (Nonempty (Path a b)) ∧ (Nonempty (Path b a)) :=
  (StronglyConnectedComponent.eq (a := a) (b := b)).1 h

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