neighborSet_singletonSubgraph — Mathlib

English

For every v ∈ V and every w ∈ V, the neighbor set of w in the subgraph consisting of only v is empty.

Русский

Для любых вершин v и w множества соседей вершины w в подграфе, содержащем лишь вершину v, пусто.

LaTeX

$$$(G.\\mathrm{singletonSubgraph}(v)).\\mathrm{neighborSet}(w) = \\emptyset$$$

Lean4

@[simp]
theorem neighborSet_singletonSubgraph (v w : V) : (G.singletonSubgraph v).neighborSet w = ∅ :=
  rfl

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