neighborSet_sSup — Mathlib

English

The neighbor set of the supremum at v is the union over s of the neighbor sets at v of each subgraph in s.

Русский

Множество соседей вершины v в наибольшем подграфе есть объединение множеств соседей v во всех подграфах из s.

LaTeX

$$$ (sSup s).neighborSet v = \\bigcup G' ∈ s, neighborSet G' v $$$

Lean4

@[simp]
theorem neighborSet_sSup (s : Set G.Subgraph) (v : V) : (sSup s).neighborSet v = ⋃ G' ∈ s, neighborSet G' v :=
  by
  ext
  simp

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