induce_deleteIncidenceSet_of_notMem

English

If x is not in the vertex set s, then the induced subgraph of G deleteIncidenceSet x on s equals the induced subgraph of G on s.

Русский

Если x ∉ s, то индуцированный подграф G\setminus Incidence(x) на s совпадает с индуцированным подграфом G на s.

LaTeX

$$$ (G\setminus \mathrm{IncidenceSet}(x)).\mathrm{induce}(s) = G.\mathrm{induce}(s) \quad \text{when } x \notin s $$$

Lean4

/-- If the vertex `x` is not in the set `s`, then the induced subgraph in `G.deleteIncidenceSet x`
by `s` is equal to the induced subgraph in `G` by `s`. -/
theorem induce_deleteIncidenceSet_of_notMem (G : SimpleGraph V) {s : Set V} {x : V} (h : x ∉ s) :
    (G.deleteIncidenceSet x).induce s = G.induce s := by
  ext v₁ v₂
  simp_rw [comap_adj, Function.Embedding.coe_subtype, deleteIncidenceSet_adj, and_iff_left_iff_imp]
  exact fun _ ↦ ⟨v₁.prop.ne_of_notMem h, v₂.prop.ne_of_notMem h⟩

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