neighborSet_subgraphOfAdj_subset — Mathlib

English

For any u, the neighbor set in the subgraph of adjacency is contained in {v, w}.

Русский

Для любого u множество соседей в подграфе по hvw содержится в {v, w}.

LaTeX

$$$(G.\\mathrm{subgraphOfAdj}(hvw)).\\mathrm{neighborSet}(u) \\subseteq \\{ v, w \\}$$$

Lean4

theorem neighborSet_subgraphOfAdj_subset {u v w : V} (hvw : G.Adj v w) :
    (G.subgraphOfAdj hvw).neighborSet u ⊆ { v, w } :=
  (G.subgraphOfAdj hvw).neighborSet_subset_verts _

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