English
The edge set of the induced subgraph on a subset s, mapped back to the ambient vertex set, equals the intersection of the original edge set with pairs from s.
Русский
Множество рёбер индуцированного подграфа на s, отображённое в исходный набор вершин, равно пересечению множества рёбер графа с парами из s.
LaTeX
$$(G.induce s).edgeFinset.map (Embedding.subtype s).sym2Map = G.edgeFinset ∩ s.toFinset.sym2$$
Lean4
theorem map_edgeFinset_induce [DecidableEq V] :
(G.induce s).edgeFinset.map (Embedding.subtype s).sym2Map = G.edgeFinset ∩ s.toFinset.sym2 :=
by
simp_rw [Finset.ext_iff, Sym2.forall, mem_inter, mk_mem_sym2_iff, mem_map, Sym2.exists, Set.mem_toFinset, mem_edgeSet,
comap_adj, Embedding.sym2Map_apply, Embedding.coe_subtype, Sym2.map_pair_eq, Sym2.eq_iff]
intro v w
constructor
· rintro ⟨x, y, hadj, ⟨hv, hw⟩ | ⟨hw, hv⟩⟩
all_goals rw [← hv, ← hw]
· exact ⟨hadj, x.prop, y.prop⟩
· exact ⟨hadj.symm, y.prop, x.prop⟩
· intro ⟨hadj, hv, hw⟩
use ⟨v, hv⟩, ⟨w, hw⟩, hadj
tauto
