English
Two graphs G1 and G2 are equal if they have the same vertex set and the same incidence relation Inc for all edges and vertices.
Русский
Два графа G1 и G2 равны, если у них одинаковое множество вершин и одинаковое отношение Inc для всех ребер и вершин.
LaTeX
$$$\\text{ext\_inc}\\ G_1\\ G_2:\\ V(G_1)=V(G_2)\\land \\forall e\\ x,\\ G_1.Inc e x\\leftrightarrow G_2.Inc e x\\Rightarrow G_1=G_2$$$
Lean4
/-- Two graphs with the same vertex set and unary incidences are equal. -/
theorem ext_inc {G₁ G₂ : Graph α β} (hV : V(G₁) = V(G₂)) (h : ∀ e x, G₁.Inc e x ↔ G₂.Inc e x) : G₁ = G₂ :=
Graph.ext hV fun _ _ _ ↦ by simp_rw [isLink_iff_inc, h]
