English
A variant cardinal equality relating induced subgraphs on complements and deletions holds in the presence of appropriate finiteness assumptions.
Русский
Существуют вариативные равенства кардинальности для индуцированных подграфов над дополнениями и удалениями с учётом ограниченности.
LaTeX
$$$ \#(G.induce(\{x\}^c).edgeFinset) = \#(G.deleteIncidenceSet x).edgeFinset $$$
Lean4
/-- The support of `G.deleteIncidenceSet x` is at most `1` less than the support of the simple
graph `G`. -/
theorem card_support_deleteIncidenceSet (G : SimpleGraph V) [DecidableRel G.Adj] {x : V} (hx : x ∈ G.support) :
card (G.deleteIncidenceSet x).support ≤ card G.support - 1 :=
by
rw [← Set.singleton_subset_iff, ← Set.toFinset_subset_toFinset] at hx
simp_rw [← Set.card_singleton x, ← Set.toFinset_card, ← card_sdiff_of_subset hx, ← Set.toFinset_diff]
apply card_le_card
rw [Set.toFinset_subset_toFinset]
exact G.support_deleteIncidenceSet_subset x
