mk'_mem_edges_singleton — Mathlib

English

If u and v are adjacent in G, then the single-edge walk from u to v contains the edge s(u,v) in its edge set.

Русский

Пусть вершины u и v соседствуют в графе G. Единичный путь от u до v включает ребро s(u,v) в множество своих ребер.

LaTeX

$$$ \forall {V} {G : SimpleGraph V} {u v : V} (h : G.Adj u v), s(u,v) \in (singleton h : G.Walk u v).edges$$$

Lean4

theorem mk'_mem_edges_singleton {u v : V} (h : G.Adj u v) : s(u, v) ∈ (singleton h : G.Walk u v).edges := by
  simp [singleton]

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