English
Taking the coe of a deleted-edges subgraph equals deleting corresponding edges in the coe-subgraph, after mapping endpoints appropriately.
Русский
Переход к отображению сопряжённого подграфа после удаления рёбер эквивалентен удалению соответствующих рёбер в сопряжённом подграфе с соответствующим отображением вершин.
LaTeX
$$$ G'.\\mathrm{coe}.\\mathrm{deleteEdges} s = (G'.\\mathrm{deleteEdges} (\\mathrm{Sym2.map}(\\uparrow)\\, ''\\, s)).\\mathrm{coe} $$$
Lean4
theorem deleteEdges_coe_eq (s : Set (Sym2 G'.verts)) :
G'.coe.deleteEdges s = (G'.deleteEdges (Sym2.map (↑) '' s)).coe :=
by
ext ⟨v, hv⟩ ⟨w, hw⟩
simp only [SimpleGraph.deleteEdges_adj, coe_adj, deleteEdges_adj, Set.mem_image, not_exists, not_and,
and_congr_right_iff]
intro
constructor
· intro hs
refine Sym2.ind ?_
rintro ⟨v', hv'⟩ ⟨w', hw'⟩
simp only [Sym2.map_pair_eq, Sym2.eq]
contrapose!
rintro (_ | _) <;> simpa only [Sym2.eq_swap]
· intro h' hs
exact h' _ hs rfl
