coe_deleteEdges_le — Mathlib

English

Deleting edges commutes with coercion: the edge-augmented subgraph after deletion corresponds to deleting in the edge-augmented graph and then coercing back.

Русский

Удаление рёбер коммутирует с отображением: получившийся после удаления граф приводится к исходному через коэрцирование.

LaTeX

$$$ (G'.deleteEdges s).\\mathrm{coe} = G'.\\mathrm{coe}.\\mathrm{deleteEdges}(\\mathrm{Sym2.map}(\\uparrow)^{-1} s) $$$

Lean4

theorem coe_deleteEdges_le : (G'.deleteEdges s).coe ≤ (G'.coe : SimpleGraph G'.verts) :=
  by
  intro v w
  simp +contextual

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