ForestRepresentation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Every finite acyclic graph has a labeled ordered-forest representation.

theorem OAI.TwoPointCorrelations.exists_forest_representation line 16
Source documentation
The labels are a permutation of the vertices and adjacency is exactly parent/child incidence in the ordered forest.
```
theorem exists_forest_representation {V : Type u} [Fintype V]
    (G : SimpleGraph V) (hG : G.IsAcyclic) :
    ∃ t : BinaryTree V, (forestNodes t).Nodup ∧ (∀ v, v ∈ forestNodes t) ∧
      ∀ a b, forestAdjacent t a b ↔ G.Adj a b := by
…
```
Mentions: OAI.TwoPointCorrelations.forestNodes, OAI.TwoPointCorrelations.forestAdjacent
lemma OAI.TwoPointCorrelations.forest_representation_numNodes line 110