English
If there exist paths a → b and b → a, then the representatives mk a and mk b are equal in the StronglyConnectedComponent.
Русский
Если существуют пути a → b и b → a, то mk a = mk b в StronglyConnectedComponent.
LaTeX
$$$ \\text{Nonempty}(\\text{Path}(a,b)) \\rightarrow \\text{Nonempty}(\\text{Path}(b,a)) \\rightarrow \\text{Eq}(\\text{StronglyConnectedComponent.mk } a)(\\text{StronglyConnectedComponent.mk } b) $$$
Lean4
theorem stronglyConnectedComponent_singleton_iff (v : V) :
(∀ w : V, (w : StronglyConnectedComponent V) = v → w = v) ↔
(∀ w : V, w ≠ v → ¬(Nonempty (Path v w) ∧ Nonempty (Path w v))) :=
by
constructor
· intro h_singleton w hw_ne h_bidir
obtain ⟨hab, hba⟩ := h_bidir
have h_same_scc : (w : StronglyConnectedComponent V) = v :=
stronglyConnectedComponent_eq_of_path (a := w) (b := v) hba hab
obtain ⟨rfl⟩ := h_singleton w h_same_scc
contradiction
· intro h_no_bidir w h_same_scc
by_contra hw_ne
obtain ⟨hab, hba⟩ := exists_path_of_stronglyConnectedComponent_eq (a := w) (b := v) h_same_scc
exact (h_no_bidir w hw_ne) ⟨hba, hab⟩
