YusterEdgeType

@[reducible, inline]

abbrev Nibble.YusterE.EdgeV {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Type u_1

The edge vertex type of G: its edges, viewed as 2-cliques. A Fintype of card |E(G)|.

Equations

• Nibble.YusterE.EdgeV G = ↥(G.cliqueFinset 2)

theorem Nibble.YusterE.card_EdgeV {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Fintype.card (EdgeV G) = (G.cliqueFinset 2).card

The edge vertex type has cardinality |E(G)| (the number of edges).

def Nibble.YusterE.triangleHypergraphSub {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Finset (Finset (EdgeV G))

The triangle hypergraph on the edge vertex type: each triangle contributes the hyperedge of its three edges (its 2-subsets, lifted to the edge type).

Equations

• Nibble.YusterE.triangleHypergraphSub G = Finset.image (fun (t : Finset V) => Finset.subtype (fun (x : Finset V) => x ∈ G.cliqueFinset 2) (Finset.powersetCard 2 t)) (G.cliqueFinset 3)

theorem Nibble.YusterE.powersetCard_two_subset_cliqueFinset {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {t : Finset V} (ht : G.IsNClique 3 t) : Finset.powersetCard 2 t ⊆ G.cliqueFinset 2

Every 2-subset of a 3-clique is a 2-clique (an edge).

theorem Nibble.YusterE.triangleHypergraphSub_uniform {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Hypergraph.IsUniform (triangleHypergraphSub G) 3

The edge-type triangle hypergraph is 3-uniform.

theorem Nibble.YusterE.triangleHypergraphSub_codegree_le_one {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {E E' : EdgeV G} (hne : E ≠ E') : Hypergraph.codegree (triangleHypergraphSub G) E E' ≤ 1

Codegree ≤ 1 on the edge-type triangle hypergraph. Two distinct edges lie in at most one common triangle. This is the (sharp) CodegreeBounded input for NibbleTheorem on the correct vertex type.