CoreGapRectPack #
The vertex-pair rectangle of a sub-triple: all ordered pairs joining two different parts
of (A, B, C).
Instances For
theorem
Nibble.AX1.tripleGraph_edgeDisjoint_of_rect_disjoint
{V : Type}
[DecidableEq V]
(G : SimpleGraph V)
{A B C A' B' C' : Finset V}
(h : Disjoint (tripleRect A B C) (tripleRect A' B' C'))
(x y : V)
(hxy : (tripleGraph G A B C).Adj x y)
:
¬(tripleGraph G A' B' C').Adj x y
Disjoint rectangles give edge-disjoint tripartite graphs.
theorem
Nibble.AX1.card_tripleRect
{V : Type}
[DecidableEq V]
{A B C : Finset V}
(hAB : Disjoint A B)
(hAC : Disjoint A C)
(hBC : Disjoint B C)
:
The area of the rectangle of a sub-triple with pairwise disjoint parts.
theorem
Nibble.AX1.sum_area_le_of_rect_disjoint_nat
{V : Type}
[Fintype V]
[DecidableEq V]
{k : ℕ}
(A B C : ℕ → Finset V)
(hAB : ∀ i < k, Disjoint (A i) (B i))
(hAC : ∀ i < k, Disjoint (A i) (C i))
(hBC : ∀ i < k, Disjoint (B i) (C i))
(hdisj : ∀ i < k, ∀ j < k, i ≠ j → Disjoint (tripleRect (A i) (B i) (C i)) (tripleRect (A j) (B j) (C j)))
:
The areas of pairwise disjoint rectangles add up to at most |V|² (natural-number form).
theorem
Nibble.AX1.sum_area_le_of_rect_disjoint
{V : Type}
[Fintype V]
[DecidableEq V]
{k : ℕ}
(A B C : ℕ → Finset V)
(hAB : ∀ i < k, Disjoint (A i) (B i))
(hAC : ∀ i < k, Disjoint (A i) (C i))
(hBC : ∀ i < k, Disjoint (B i) (C i))
(hdisj : ∀ i < k, ∀ j < k, i ≠ j → Disjoint (tripleRect (A i) (B i) (C i)) (tripleRect (A j) (B j) (C j)))
:
The areas of pairwise disjoint rectangles add up to at most |V|².