English
The cardinality of the edgeFinset of the induced subgraph on the complement of {x} equals the cardinality of the edgeFinset of G.deleteIncidenceSet x.
Русский
Число ребер индуцированного подграфа на дополнении {x} равно числу ребер графа после удаления инцидентного множества x.
LaTeX
$$$ \#(G.induce(\{x\}^c)).edgeFinset = \#(G.deleteIncidenceSet x).edgeFinset $$$
Lean4
/-- Deleting the incidence set of the vertex `x` retains the same number of edges as in the induced
subgraph of the vertices `{x}ᶜ`. -/
theorem card_edgeFinset_induce_compl_singleton (G : SimpleGraph V) [DecidableRel G.Adj] (x : V) :
#(G.induce { x }ᶜ).edgeFinset = #(G.deleteIncidenceSet x).edgeFinset :=
by
have h_notMem : x ∉ ({ x }ᶜ : Set V) := Set.notMem_compl_iff.mpr (Set.mem_singleton x)
simp_rw [Set.toFinset_card, ← G.induce_deleteIncidenceSet_of_notMem h_notMem, ← Set.toFinset_card]
apply card_edgeFinset_induce_of_support_subset
trans G.support \ { x }
· exact support_deleteIncidenceSet_subset G x
· rw [Set.compl_eq_univ_diff]
exact Set.diff_subset_diff_left (Set.subset_univ G.support)
