English
The image of the coe-edgeSet under the map Sym2.map Subtype.val equals the underlying edge set of the subgraph.
Русский
Образ множества ребер подграфа через отображение Sym2.map равен исходному множеству ребер подграфа.
LaTeX
$$$\\mathrm{Sym2.map}(\\mathrm{Subtype.val})[G'.\\mathrm{coe}.\\mathrm{edgeSet}] = G'.\\mathrm{edgeSet}$$$
Lean4
theorem image_coe_edgeSet_coe (G' : G.Subgraph) : Sym2.map (↑) '' G'.coe.edgeSet = G'.edgeSet :=
by
rw [edgeSet_coe, Set.image_preimage_eq_iff]
rintro e he
induction e using Sym2.ind with
| h a b =>
rw [Subgraph.mem_edgeSet] at he
exact ⟨s(⟨a, edge_vert _ he⟩, ⟨b, edge_vert _ he.symm⟩), Sym2.map_pair_eq ..⟩