English
The graph determined by the vertex set V(G), the incidence relation IsLink, and an edge set E defined by E = { e : β | ∃ x y, G.IsLink e x y } is equal to G.
Русский
Граф, определяемый множеством вершин V(G), отношением инцидиденций IsLink и множеством ребер E, где E состоит из тех ребер e, для которых существуют вершины x,y с G.IsLink e x y, равен G.
LaTeX
$$$E = \\{e\\in \\beta\\mid \\exists x,y\\, G.IsLink\\ e\\ x\\ y\\}\\;\\Rightarrow\\; Graph.mk\\ V(G)\\ G.IsLink\\ E = G$$$
Lean4
/-- `edgeSet` can be determined using `IsLink`, so the graph constructed from `G.vertexSet` and
`G.IsLink` using any value for `edgeSet` is equal to `G` itself. -/
@[simp]
theorem mk_eq_self (G : Graph α β) {E : Set β} (hE : ∀ e, e ∈ E ↔ ∃ x y, G.IsLink e x y) :
Graph.mk V(G) G.IsLink E
(by simpa [show E = E(G) by simp [Set.ext_iff, hE, G.edge_mem_iff_exists_isLink]] using G.isLink_symm)
(fun _ _ _ _ _ h h' ↦ h.left_eq_or_eq h') hE (fun _ _ _ ↦ IsLink.left_mem) =
G :=
by
obtain rfl : E = E(G) := by simp [Set.ext_iff, hE, G.edge_mem_iff_exists_isLink]
cases G with
| _ _ _ _ _ _ h _ => simp
