English
The complete bipartite graph on two vertex types V and W has all edges between the two sides and no edges within the same side.
Русский
Полный двудольный граф на двух множествах вершин V и W имеет все ребра между двумя частями и не имеет ребер внутри одной части.
LaTeX
$$$ \\mathrm{Adj}_{K}(\\mathrm{inl}(v),\\mathrm{inr}(w)) \\iff \\text{(}v\\text{ isLeft} \\land w\\text{ isRight)} \\lor (v\\text{ isRight} \\land w\\text{ isLeft}). $$$$
Lean4
/-- Two vertices are adjacent in the complete bipartite graph on two vertex types
if and only if they are not from the same side.
Any bipartite graph may be regarded as a subgraph of one of these. -/
@[simps]
def completeBipartiteGraph (V W : Type*) : SimpleGraph (V ⊕ W)
where
Adj v w := v.isLeft ∧ w.isRight ∨ v.isRight ∧ w.isLeft
symm v w := by cases v <;> cases w <;> simp
loopless v := by cases v <;> simp
