neighborSet_subset — Mathlib

English

For any subgraph G' of G and any vertex v, the neighbor set in G' is a subset of the neighbor set in G.

Русский

Для любого подграфа G' графа G и вершины v множество соседей в G' является подмножеством множества соседей в G.

LaTeX

$$$G'.neighborSet(v) \\subseteq G.neighborSet(v)$$$

Lean4

theorem neighborSet_subset (G' : Subgraph G) (v : V) : G'.neighborSet v ⊆ G.neighborSet v := fun _ ↦ G'.adj_sub

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