English
There is an equivalence between the incidence set at a vertex and its neighbor set, implemented by the maps described above.
Русский
Существует эквивалентность между множеством инцидентности вершины и её множеством соседей, реализуемая указанными выше отображениями.
LaTeX
$$$\text{Equiv}(\mathrm{Incidence}_G(v), G.\mathrm{neighborSet}(v)).$$$
Lean4
/-- There is an equivalence between the set of edges incident to a given
vertex and the set of vertices adjacent to the vertex. -/
@[simps]
def incidenceSetEquivNeighborSet (v : V) : G.incidenceSet v ≃ G.neighborSet v
where
toFun e := ⟨G.otherVertexOfIncident e.2, G.incidence_other_prop e.2⟩
invFun w := ⟨s(v, w.1), G.mem_incidence_iff_neighbor.mpr w.2⟩
left_inv x := by simp [otherVertexOfIncident]
right_inv := fun ⟨w, hw⟩ => by
simp only [Subtype.mk.injEq]
exact incidence_other_neighbor_edge _ hw
