neighborSet_fst_subgraphOfAdj — Mathlib

English

For all u, the neighbor set in the subgraph of adjacency hvw is the union of at most two singletons: {w} if u=v and {v} if u=w.

Русский

Для всех u множество соседей в подграфе hvw равно объединению максимум двух одноэлементных множеств: {w} при u=v и {v} при u=w.

LaTeX

$$$ (G.\\mathrm{subgraphOfAdj}(hvw)).\\mathrm{neighborSet}(u) = (\\text{if } u = v \\text{ then } \\{ w \\} \\text{ else } \\emptyset) \\cup (\\text{if } u = w \\text{ then } \\{ v \\} \\text{ else } \\emptyset)$$$

Lean4

@[simp]
theorem neighborSet_fst_subgraphOfAdj {v w : V} (hvw : G.Adj v w) : (G.subgraphOfAdj hvw).neighborSet v = { w } :=
  by
  ext u
  suffices w = u ↔ u = w by simpa [hvw.ne.symm] using this
  rw [eq_comm]

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