card_neighborFinset_union_of_adj — Mathlib

English

If two vertices v,w are 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_adj {v w} (h : G.IsSRGWith n k ℓ μ) (ha : G.Adj v w) : #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - ℓ$$

Lean4

theorem card_neighborFinset_union_of_adj {v w : V} (h : G.IsSRGWith n k ℓ μ) (ha : G.Adj v w) :
    #(G.neighborFinset v ∪ G.neighborFinset w) = 2 * k - ℓ :=
  by
  rw [← h.of_adj v w ha]
  exact h.card_neighborFinset_union_eq

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