deleteEdges_le_of_le — Mathlib

English

If s ⊆ s', then deleting s' edges yields a subgraph contained in deleting s edges.

Русский

Если s ⊆ s', то удаление рёбер s' даёт подграф, содержащийся в подграфе, полученном удалением s.

LaTeX

$$$ s \\subseteq s' \\Rightarrow G'.deleteEdges(s') \\le G'.deleteEdges(s) $$$

Lean4

theorem deleteEdges_le_of_le {s s' : Set (Sym2 V)} (h : s ⊆ s') : G'.deleteEdges s' ≤ G'.deleteEdges s :=
  by
  constructor <;> simp +contextual only [deleteEdges_verts, deleteEdges_adj, true_and, and_imp, subset_rfl]
  exact fun _ _ _ hs' hs ↦ hs' (h hs)

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