reachable_is_equivalence — Mathlib

English

Reachability is an equivalence relation on the vertex set: reflexive, symmetric, and transitive.

Русский

Достижимость образует эквивалентность на множестве вершин: рефлексивность, симметричность и транзитивность.

LaTeX

$$$\text{Equivalence } G.Reachable.$$$

Lean4

theorem reachable_is_equivalence : Equivalence G.Reachable :=
  Equivalence.mk (@Reachable.refl _ G) (@Reachable.symm _ G) (@Reachable.trans _ G)

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