mk_eq_mk — Mathlib

English

Equality of the representatives of a and b in the StronglyConnectedComponent is equivalent to the existence of paths both from a to b and from b to a.

Русский

Равенство представителей a и b в StronglyConnectedComponent эквивалентно существованию путей из a в b и из b в a.

LaTeX

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

Lean4

@[simp]
theorem mk_eq_mk {a b : V} :
    (StronglyConnectedComponent.mk a : StronglyConnectedComponent V) = StronglyConnectedComponent.mk b ↔
      (Nonempty (Path a b) ∧ Nonempty (Path b a)) :=
  StronglyConnectedComponent.eq a b

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