adj_iff_exists_edge_coe — Mathlib

English

Adjacency is equivalent to the existence of an edge whose value matches the pair (a,b).

Русский

Смежность эквивалентна существованию ребра, значение которого равно паре (a,b).

LaTeX

$$$$ G.Adj a b \iff \exists e : G.edgeSet, e.val = s(a,b). $$$$

Lean4

theorem adj_iff_exists_edge_coe : G.Adj a b ↔ ∃ e : G.edgeSet, e.val = s(a, b) := by
  simp only [mem_edgeSet, exists_prop, SetCoe.exists, exists_eq_right]

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