English
Two vertices are adjacent iff there exists an edge between them, with v ≠ w.
Русский
Две вершины смежны тогда и только тогда, когда между ними существует ребро, причём вершины различны.
LaTeX
$$$$ G.Adj(v,w) \iff (v \neq w) \land \exists e \in E(G), v \in e \land w \in e. $$$$
Lean4
/-- Two vertices are adjacent iff there is an edge between them. The
condition `v ≠ w` ensures they are different endpoints of the edge,
which is necessary since when `v = w` the existential
`∃ (e ∈ G.edgeSet), v ∈ e ∧ w ∈ e` is satisfied by every edge
incident to `v`. -/
theorem adj_iff_exists_edge {v w : V} : G.Adj v w ↔ v ≠ w ∧ ∃ e ∈ G.edgeSet, v ∈ e ∧ w ∈ e :=
by
refine ⟨fun _ => ⟨G.ne_of_adj ‹_›, s(v, w), by simpa⟩, ?_⟩
rintro ⟨hne, e, he, hv⟩
rw [Sym2.mem_and_mem_iff hne] at hv
subst e
rwa [mem_edgeSet] at he
