OAI/Combinatorics/CliqueFree/Splitting.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CliqueFreeIndependence.WeightedGraph.Splitting.graph line 23
2. lemma OAI.CliqueFreeIndependence.WeightedGraph.Splitting.projection line 39
3. lemma OAI.CliqueFreeIndependence.WeightedGraph.Splitting.neighborMass_le line 58
4. def OAI.CliqueFreeIndependence.WeightedGraph.Splitting.Survives line 93

   Source documentation

   All three corner agreements and all six admissible incidences.

   def Survives (F : EdgeState G → EdgeState G) (good : EdgeState G → Prop)
       (t : TriangleState G) : Prop :=
   …

   Mentions: OAI.CliqueFreeIndependence.WeightedGraph.EdgeState, OAI.CliqueFreeIndependence.WeightedGraph.TriangleState

5. lemma OAI.CliqueFreeIndependence.WeightedGraph.Splitting.triangleMass_surviving_le line 101