deleteVerts_deleteVerts — Mathlib

English

Deleting s then s' from G' yields the same as deleting s ∪ s' at once: (G'.deleteVerts s).deleteVerts s' = G'.deleteVerts (s ∪ s').

Русский

Удаление s затем s' из G' эквивалентно удалению s ∪ s' сразу: (G'.deleteVerts s).deleteVerts s' = G'.deleteVerts (s ∪ s').

LaTeX

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

Lean4

@[simp]
theorem deleteVerts_deleteVerts (s s' : Set V) : (G'.deleteVerts s).deleteVerts s' = G'.deleteVerts (s ∪ s') := by
  ext <;> simp +contextual [not_or, and_assoc]

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