English
If H ≠ ⊥, then G.killCopies H = G iff H.Free G.
Русский
Если H ≠ ⊥, то G.killCopies H = G тогда и только тогда, когда HFree G.
LaTeX
$$G.killCopies(H) = G \iff H.Free G$$
Lean4
/-- `G.killCopies H` has no effect on `G` if and only if `G` already contained no copies of `H`. See
`Free.killCopies_eq_left` for the reverse implication with no assumption on `H`. -/
theorem killCopies_eq_left (hH : H ≠ ⊥) : G.killCopies H = G ↔ H.Free G :=
by
simp only [killCopies_of_ne_bot hH, Set.disjoint_left, isContained_iff_exists_iso_subgraph, @forall_swap _ G.Subgraph,
deleteEdges_eq_self, Set.mem_iUnion, not_exists, not_nonempty_iff, Nonempty.forall, Free]
exact
forall_congr' fun G' ↦
⟨fun h ↦ ⟨fun f ↦ h _ (Subgraph.edgeSet_subset _ <| (aux hH ⟨f⟩).choose_spec) f rfl⟩, fun h _ _ ↦ h.elim⟩
