support_deleteIncidenceSet_subset

English

The support of the graph after deleting the incidence set of x is contained in the support of G with x removed.

Русский

Поддержка графа после удаления инцидентного множества x содержится в поддержке G без x.

LaTeX

$$$ \mathrm{supp}(G\setminus \mathrm{IncidenceSet}(x)) \subseteq \mathrm{supp}(G) \setminus \{x\} $$$

Lean4

/-- The support of `G.deleteIncidenceSet x` is a subset of the support of `G` set difference the
singleton set `{x}`. -/
theorem support_deleteIncidenceSet_subset (G : SimpleGraph V) (x : V) :
    (G.deleteIncidenceSet x).support ⊆ G.support \ { x } := fun _ ↦ by simp_rw [mem_support, deleteIncidenceSet_adj];
  tauto

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