toSimpleGraphStrict_subgraph_toSimpleGraphInclusive

English

The subgraph order respects inclusion of edge sets: a subgraph is contained in another when its adjacency is contained in the other's.

Русский

Порядок подграфа соответствует включению множеств ребер: подграф содержится в другом, если его смежность включена во смежность другого.

LaTeX

$$$G^{\\text{toStrict}} \\le G^{\\text{toInclusive}}$$$

Lean4

theorem toSimpleGraphStrict_subgraph_toSimpleGraphInclusive (G : Digraph V) :
    G.toSimpleGraphStrict ≤ G.toSimpleGraphInclusive := fun _ _ h ↦ ⟨h.1, Or.inl h.2.1⟩

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