neighborSet_subgraphOfAdj — Mathlib

English

If hvw holds and u is not equal to both v and w, then the neighbor set of u in the subgraphOfAdj hvw is empty.

Русский

Если hvw выполняется и u не равно ни v, ни w, то у множеству соседей в подграфе hvw пусто.

LaTeX

$$$(G.\\mathrm{subgraphOfAdj}(hvw).\\mathrm{neighborSet}(u) = \\emptyset)$$$

Lean4

theorem neighborSet_subgraphOfAdj [DecidableEq V] {u v w : V} (hvw : G.Adj v w) :
    (G.subgraphOfAdj hvw).neighborSet u = (if u = v then { w } else ∅) ∪ if u = w then { v } else ∅ := by
  split_ifs <;> subst_vars <;> simp [*]

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