English
Two graphs with the same vertex set and identical incidence relations are equal.
Русский
Два графа с одинаковым множеством вершин и идентичными отношениями инцидиденций равны.
LaTeX
$$$\\forall G_1\\ G_2:\\ Graph\\ α\\ β,\\ V(G_1)=V(G_2)\\land \\forall e\\ x\\ y,\\ G_1.IsLink e x y\\leftrightarrow G_2.IsLink e x y\\Rightarrow G_1=G_2$$$
Lean4
/-- Two graphs with the same vertex set and binary incidences are equal.
(We use this as the default extensionality lemma rather than adding `@[ext]`
to the definition of `Graph`, so it doesn't require equality of the edge sets.) -/
@[ext]
protected theorem ext {G₁ G₂ : Graph α β} (hV : V(G₁) = V(G₂)) (h : ∀ e x y, G₁.IsLink e x y ↔ G₂.IsLink e x y) :
G₁ = G₂ :=
by
rw [← G₁.mk_eq_self G₁.edge_mem_iff_exists_isLink, ← G₂.mk_eq_self G₂.edge_mem_iff_exists_isLink]
convert rfl using 2
· exact hV.symm
· simp [funext_iff, h]
simp [edgeSet_eq_setOf_exists_isLink, h]
