English
Let G be a simple graph on V and x a vertex. For any vertices v1, v2 ∈ V, the vertices v1 and v2 are adjacent in the graph obtained by deleting the incidence set of x if and only if they were adjacent in G and neither equals x.
Русский
Пусть G — простой граф на V и x — вершина. Для любых вершин v1, v2 ∈ V вершины v1 и v2 смежны в графе, полученном после удаления инцидентного множества вершины x, тогда и только тогда они смежны в G, и ни одна из них не равна x.
LaTeX
$$$ (G\setminus \mathrm{IncidenceSet}(x)).\mathrm{Adj}(v_1,v_2) \iff G.\mathrm{Adj}(v_1,v_2) \land v_1 \neq x \land v_2 \neq x $$$
Lean4
theorem deleteIncidenceSet_adj {G : SimpleGraph V} {x v₁ v₂ : V} :
(G.deleteIncidenceSet x).Adj v₁ v₂ ↔ G.Adj v₁ v₂ ∧ v₁ ≠ x ∧ v₂ ≠ x :=
by
rw [deleteIncidenceSet, deleteEdges_adj, mk'_mem_incidenceSet_iff]
tauto
