map_edgeFinset_induce_of_support_subset

English

If the support G.support is contained in s, then the induced edge Finset on s maps to the original edge Finset of G.

Русский

Если поддержка графа G лежит внутри s, индуцированное множество рёбер на s отображается в множество рёбер G.

LaTeX

$$(G.induce s).edgeFinset.map (Embedding.subtype s).sym2Map = G.edgeFinset$$

Lean4

theorem map_edgeFinset_induce_of_support_subset (h : G.support ⊆ s) :
    (G.induce s).edgeFinset.map (Embedding.subtype s).sym2Map = G.edgeFinset := by
  classical simpa [map_edgeFinset_induce] using edgeFinset_subset_sym2_of_support_subset h

Похожие утверждения