edgeFinset_deleteEdges — Mathlib

English

Deleting a set s of edges from G, the resulting edgeFinset corresponds to the SDiff of G.edgeFinset with s.

Русский

Удаление множества рёбер s из G приводит к edgeFinset, равному SDiff(G.edgeFinset, s).

LaTeX

$$ (G.deleteEdges s.toSet).edgeFinset = Finset.instSDiff.sdiff G.edgeFinset s$$

Lean4

theorem edgeFinset_deleteEdges [DecidableEq V] [Fintype G.edgeSet] (s : Finset (Sym2 V))
    [Fintype (G.deleteEdges s).edgeSet] : (G.deleteEdges s).edgeFinset = G.edgeFinset \ s :=
  by
  ext e
  simp [edgeSet_deleteEdges]

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