neighborSet_completeEquipartiteGraph

English

For any vertex v = (a,b) in the complete equipartite graph K_r(t), its neighbor set consists of all vertices whose first coordinate is different from a.

Русский

Для вершины v=(a,b) в графе K_r(t) множество соседей состоит из всех вершин с первой координатой, отличной от a.

LaTeX

$$N(v) = { (a',b') ∈ Fin r × Fin t : a' ≠ v.1 }$$

Lean4

theorem neighborSet_completeEquipartiteGraph (v) :
    (completeEquipartiteGraph r t).neighborSet v = { v.1 }ᶜ ×ˢ Set.univ := by ext; simp [ne_comm]

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