OAI/MeasureTheory/DyadicAvoidance/PreorderIndex.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem310.PreorderIndex.idxOf_map_injective line 10
2. theorem OAI.Problem310.PreorderIndex.idxOf_flatMap_uniform line 23
3. theorem OAI.Problem310.PreorderIndex.size_eq_one_add_edgeCount line 42
4. theorem OAI.Problem310.PreorderIndex.rank_eq_idxOf_add_one line 50

   Source documentation

   The arithmetic preorder rank agrees with the actual list enumeration. The root is omitted from edgePaths, hence the offset by one.

   theorem rank_eq_idxOf_add_one {K d : ℕ} {p : List (Fin K)}
       (hp : p ∈ TreePreorder.edgePaths K d) :
       TreePreorderRank.rank d p = (TreePreorder.edgePaths K d).idxOf p + 1 := by
   …

   Mentions: OAI.Problem310.TreePreorder.edgePaths, OAI.Problem310.TreePreorderRank.rank

5. theorem OAI.Problem310.PreorderIndex.edgeRank_eq_idxOf line 101