OAI/NumberTheory/TwoPoint/Bounds/PreorderNumbering.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Preorder numbering depends only on the ordered forest shape.

  1. lemma OAI.TwoPointCorrelations.forest_map_congr line 14
  2. lemma OAI.TwoPointCorrelations.forest_numNodes_map line 26
  3. def OAI.TwoPointCorrelations.numberForest line 30
  4. lemma OAI.TwoPointCorrelations.numberForest_map line 35
  5. lemma OAI.TwoPointCorrelations.numberForest_eq_map_idxOf line 39
  6. theorem OAI.TwoPointCorrelations.numberForest_eq_of_same_shape line 68

    Source documentation

    Thus erasing numerical labels preserves the canonical numbered graph.

    theorem numberForest_eq_of_same_shape (t : BinaryTree V) (s : BinaryTree W)
    (hts : t.map (fun _ => ()) = s.map (fun _ => ())) (start : ℕ) :
    numberForest t start = numberForest s start := by
…

    Mentions: OAI.TwoPointCorrelations.numberForest

  7. lemma OAI.TwoPointCorrelations.preorder_index_injective line 74
  8. theorem OAI.TwoPointCorrelations.numberForest_adjacent line 81

    Source documentation

    Numbering transports every edge without retaining its original labels.

    theorem numberForest_adjacent [DecidableEq V] (t : BinaryTree V)
    (ht : (forestNodes t).Nodup) (hcover : ∀ v, v ∈ forestNodes t) (x y : V) :
    forestAdjacent (numberForest t 0) ((forestNodes t).idxOf x) ((forestNodes t).idxOf y) ↔
      forestAdjacent t x y := by
…

    Mentions: OAI.TwoPointCorrelations.forestNodes, OAI.TwoPointCorrelations.forestAdjacent, OAI.TwoPointCorrelations.numberForest