Bipartite graph

Set

 context $V$ … set definiendum $\langle V,E\rangle \in \mathrm{it}(E,V)$ postulate $\langle V,E\rangle$ … undirected graph range $X\cup Y=V$ range $X\cap Y=\emptyset$ range $v,w\in V$ postulate $\exists X,Y.\ \forall u,v.\ \{u,v\}\in E\implies \neg(u\in X\land v\in X)\land \neg(v\in Y\land u\in Y)$

Discussion

We denote the graph $G$ with bipartition $X,Y$ by $G[X,Y]$ and call $X$ and $Y$ its parts.

Theorems

A bipartite graph $G[X,Y]$ has $n=|X|+|Y|$ vertices and so has at most $|X|\cdot|Y|=|X|\cdot(n-|X|)$ edges. With respect to maximizing edge number, the optimal situation is $|X|=|Y|=n/2$ where $n^2/4$ can be reached.

If the graph is also $k$-regular with $k\ge 1$, then automatically $|X|=|Y|$.

Since for each edge, one end lies in $X$ and one in $Y$, we have $\sum_{v\in X}d(v)=\sum_{v\in Y}d(v)$