English
Removing an edge for each subgraph isomorphic to G means that the number of edges we've removed is at most the number of copies of G in H.
Русский
Удаление ребра за каждое подобgraph-ов G не превышает количество копий G в H.
LaTeX
$$$ |E(G)| - copyCount_G(H) \le |E(G.killCopies(H))| $$$
Lean4
/-- Removing an edge from `H` for each subgraph isomorphic to `G` means that the number of edges
we've removed is at most the number of copies of `G` in `H`. -/
theorem le_card_edgeFinset_killCopies [Fintype V] : #G.edgeFinset - G.copyCount H ≤ #(G.killCopies H).edgeFinset := by
classical
obtain rfl | hH := eq_or_ne H ⊥
· simp
let f (G' : { G' : G.Subgraph // Nonempty (H ≃g G'.coe) }) := (aux hH G'.2).some
calc
_ = #G.edgeFinset - card { G' : G.Subgraph // Nonempty (H ≃g G'.coe) } := ?_
_ ≤ #G.edgeFinset - #(univ.image f) := (Nat.sub_le_sub_left card_image_le _)
_ = #G.edgeFinset - #(Set.range f).toFinset := by rw [Set.toFinset_range]
_ ≤ #(G.edgeFinset \ (Set.range f).toFinset) := le_card_sdiff ..
_ = #(G.killCopies H).edgeFinset := ?_
· simp only [Set.toFinset_card]
rw [← Set.toFinset_card, ← edgeFinset, copyCount, ← card_subtype, subtype_univ, card_univ]
simp only [killCopies_of_ne_bot, hH, Ne, not_false_iff, Set.toFinset_card, edgeSet_deleteEdges]
simp only [Finset.sdiff_eq_inter_compl, Set.diff_eq, ← Set.iUnion_singleton_eq_range, Set.coe_toFinset, coe_filter,
Set.iUnion_subtype, ← Fintype.card_coe, ← Finset.coe_sort_coe, coe_inter, coe_compl, Set.coe_toFinset,
Set.compl_iUnion, Fintype.card_ofFinset, f]
