OAI/Combinatorics/Ramsey/CycleClique/Construction/FastLayoutGraph.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A checked adjacency table gives a computable graph presentation whose edge tests require only two array lookups.

  1. def OAI.CycleClique.Construction.adjacencyTableLookup line 9
  2. def OAI.CycleClique.Construction.adjacencyTableGraph line 13

    Source documentation

    Present H by a separately checked finite adjacency table.

    def adjacencyTableGraph {n : ℕ} (H : SimpleGraph (Fin n))
    (A : Array (Array Bool))
    (hEq : ∀ i j : Fin n, H.Adj i j ↔ adjacencyTableLookup A i.val j.val = true) :
    SimpleGraph (Fin n) where
…

    Mentions: OAI.CycleClique.Construction.adjacencyTableLookup

  3. instance OAI.CycleClique.Construction.(instance at line 21) line 21
  4. theorem OAI.CycleClique.Construction.adjacencyTableGraph_eq line 26