deleteEdges_deleteEdges — Mathlib

English

Deleting edges with two sets s and s' is the same as deleting with the union s ∪ s'.

Русский

Удаление рёбер двумя множествами s и s' эквивалентно удалению рёбер множеством s ∪ s'.

LaTeX

$$$ (G'.deleteEdges(s)).deleteEdges(s') = G'.deleteEdges(s\\cup s'). $$$

Lean4

@[simp]
theorem deleteEdges_deleteEdges (s s' : Set (Sym2 V)) : (G'.deleteEdges s).deleteEdges s' = G'.deleteEdges (s ∪ s') :=
  by ext <;> simp [and_assoc, not_or]

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