English
Define the complete bipartite digraph on V and W as the digraph on the disjoint sum V ⊕ W whose arrows go exactly between the two parts: from V to W and from W to V.
Русский
Определим полный двудольный ориентированный граф на множествах V и W как граф на сумме V ⊕ W, у которого все дуги идут между двумя частями: из V в W и из W в V.
LaTeX
$$$\\mathrm{Adj}(a,b) \\iff a\\in V \\land b\\in W \\lor a\\in W \\land b\\in V$ for $a,b \\in V\\sqcup W$.$$
Lean4
/-- Two vertices are adjacent in the complete bipartite digraph on two vertex types
if and only if they are not from the same side.
Any bipartite digraph may be regarded as a subgraph of one of these.
-/
@[simps]
def completeBipartiteGraph (V W : Type*) : Digraph (Sum V W) where
Adj v w := v.isLeft ∧ w.isRight ∨ v.isRight ∧ w.isLeft
