reachable_iff_reflTransGen — Mathlib

English

For any vertices u,v, G.Reachable u v is equivalent to the reflexive transitive closure of G.Adj.

Русский

Для любых вершин u,v достижимость G.Reachable u v эквивалентна рефлексивному транситному закрытию adjacency.

LaTeX

$$$G.Reachable u v \iff (\text{Relation.ReflTransGen } G.Adj)\; u\; v.$$$

Lean4

theorem reachable_iff_reflTransGen (u v : V) : G.Reachable u v ↔ Relation.ReflTransGen G.Adj u v :=
  by
  constructor
  · rintro ⟨h⟩
    induction h with
    | nil => rfl
    | cons h' _ ih => exact (Relation.ReflTransGen.single h').trans ih
  · intro h
    induction h with
    | refl => rfl
    | tail _ ha hr => exact Reachable.trans hr ⟨Walk.cons ha Walk.nil⟩

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