neighborSet_inf — Mathlib

English

The neighbor set at v in the infimum equals the intersection of neighbor sets at v and the intersection with G's neighbor set.

Русский

Множество соседей вершины v в пересечении подграфов равно пересечению множеств соседей G' на v с множеством соседей G.

LaTeX

$$$ (H \\sqcap H').neighborSet v = H.neighborSet v \\cap H'.neighborSet v $$$

Lean4

@[simp]
theorem neighborSet_inf {H H' : G.Subgraph} (v : V) : (H ⊓ H').neighborSet v = H.neighborSet v ∩ H'.neighborSet v :=
  rfl

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