neighborSet_sup — Mathlib

English

The neighbor set at v in the supremum equals the union of the neighbor sets at v in H and H'.

Русский

Множество соседей вершины v в наибольшем подграфе H ⊔ H' равно объединению множеств соседей в H и в H'.

LaTeX

$$$ (H \\sqcup H').neighborSet v = H.neighborSet v \\\\cup H'.neighborSet v $$$

Lean4

@[simp]
theorem neighborSet_sup {H H' : G.Subgraph} (v : V) : (H ⊔ H').neighborSet v = H.neighborSet v ∪ H'.neighborSet v :=
  rfl

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