def SimpleGraph.johnson (n k : ℕ) : SimpleGraph { s : Finset (Fin n) // s.card = k }

The Johnson graph $J(n, k)$ has as vertices the $k$-subsets of an $n$-set. Two vertices are adjacent if their intersection has size $k - 1$.

Equations

• SimpleGraph.johnson n k = { Adj := fun (s t : { s : Finset (Fin n) // s.card = k }) => (↑s ∩ ↑t).card + 1 = k, symm := ⋯, loopless := ⋯ }

theorem SimpleGraph.johnson_adj (n k : ℕ) (s t : { s : Finset (Fin n) // s.card = k }) : (johnson n k).Adj s t = ((↑s ∩ ↑t).card + 1 = k)

def SimpleGraph.«termJ(_,_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.johnson_adj_iff_ge {n k : ℕ} {s t : { s : Finset (Fin n) // s.card = k }} : (johnson n k).Adj s t ↔ s ≠ t ∧ k ≤ (↑s ∩ ↑t).card + 1

theorem SimpleGraph.not_johnson_adj_iff_lt {n k : ℕ} {s t : { s : Finset (Fin n) // s.card = k }} : ¬(johnson n k).Adj s t ↔ s = t ∨ (↑s ∩ ↑t).card + 1 < k