card_neighborFinset_union_of_not_adj

English

If two vertices v,w are not adjacent in a strongly regular graph, then the union of their neighbor sets has size 2k minus μ.

Русский

Если вершины v и w не смежны в графе со строгой регулярностью, то размер объединения их множеств соседей равен 2k − μ.

LaTeX

$$card_neighborFinset_union_of_not_adj {v w} (h : G.IsSRGWith n k ℓ μ) (hne : v ≠ w) (ha : ¬G.Adj v w) : #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - μ$$

Lean4

/-- Assuming `G` is strongly regular, `2*(k + 1) - m` in `G` is the number of vertices that are
adjacent to either `v` or `w` when `¬G.Adj v w`. So it's the cardinality of
`G.neighborSet v ∪ G.neighborSet w`. -/
theorem card_neighborFinset_union_of_not_adj {v w : V} (h : G.IsSRGWith n k ℓ μ) (hne : v ≠ w) (ha : ¬G.Adj v w) :
    #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - μ :=
  by
  rw [← h.of_not_adj hne ha]
  exact h.card_neighborFinset_union_eq

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