TripleEdges #
theorem
Nibble.AX1.interedges_card_le_tripleGraph_edges
{V : Type}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(A B C : Finset V)
(hAB : Disjoint A B)
:
The A–B edges of G are edges of the tripartite graph of (A, B, C). They inject
into its 2-cliques (injectively, because A and B are disjoint, so an unordered pair
determines which endpoint lies in A).
theorem
Nibble.AX1.edgeDensity_mul_le_tripleGraph_edges
{V : Type}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(A B C : Finset V)
(hAB : Disjoint A B)
:
Density form of Nibble.AX1.interedges_card_le_tripleGraph_edges.
TripleEdgesThree #
theorem
Nibble.AX1.three_interedges_card_le_tripleGraph_edges
{V : Type}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(A B C : Finset V)
(hAB : Disjoint A B)
(hAC : Disjoint A C)
(hBC : Disjoint B C)
:
(G.interedges A B).card + (G.interedges A C).card + (G.interedges B C).card ≤ ((tripleGraph G A B C).cliqueFinset 2).card
All three pairs of a sub-triple contribute to its edge count.
theorem
Nibble.AX1.three_edgeDensity_mul_le_tripleGraph_edges
{V : Type}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(A B C : Finset V)
(hAB : Disjoint A B)
(hAC : Disjoint A C)
(hBC : Disjoint B C)
:
↑(G.edgeDensity A B) * ↑A.card * ↑B.card + ↑(G.edgeDensity A C) * ↑A.card * ↑C.card + ↑(G.edgeDensity B C) * ↑B.card * ↑C.card ≤ ↑((tripleGraph G A B C).cliqueFinset 2).card
Density form: the lower bound for the number of edges of a sub-triple used by the design.