OAI/Analysis/Nonexpansive/OrderedTree.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Ordered trees with finite nonempty levels

The parent maps are monotone surjections. Thus every node has children, and the children of consecutive parents occur in consecutive groups. Ancestor maps are actual finite composites of parent maps.

  1. structure OAI.ReflexiveFixedPoints.OrderedTree line 17
  2. abbrev OAI.ReflexiveFixedPoints.OrderedTree.Node line 27
  3. def OAI.ReflexiveFixedPoints.OrderedTree.root line 31
  4. theorem OAI.ReflexiveFixedPoints.OrderedTree.eq_root line 33
  5. def OAI.ReflexiveFixedPoints.OrderedTree.ancestorLE line 39

    Source documentation

    The ancestor at an earlier level, obtained by composing parent maps.

    def ancestorLE {i j : ℕ} (h : i ≤ j) : T.Node j → T.Node i :=
…
  6. theorem OAI.ReflexiveFixedPoints.OrderedTree.ancestorLE_refl line 43
  7. theorem OAI.ReflexiveFixedPoints.OrderedTree.ancestorLE_step line 47
  8. theorem OAI.ReflexiveFixedPoints.OrderedTree.ancestorLE_succ line 51
  9. theorem OAI.ReflexiveFixedPoints.OrderedTree.ancestorLE_trans line 56
  10. theorem OAI.ReflexiveFixedPoints.OrderedTree.ancestorLE_refl_apply line 65
  11. theorem OAI.ReflexiveFixedPoints.OrderedTree.ancestorLE_step_apply line 70
  12. theorem OAI.ReflexiveFixedPoints.OrderedTree.ancestorLE_succ_apply line 75
  13. theorem OAI.ReflexiveFixedPoints.OrderedTree.ancestorLE_trans_apply line 79
  14. theorem OAI.ReflexiveFixedPoints.OrderedTree.ancestorLE_monotone line 86
  15. theorem OAI.ReflexiveFixedPoints.OrderedTree.ancestorLE_surjective line 94
  16. def OAI.ReflexiveFixedPoints.OrderedTree.descendants line 105

    Source documentation

    The later-level descendants of a node.

    def descendants {i j : ℕ} (h : i ≤ j) (v : T.Node i) : Finset (T.Node j) :=
…
  17. theorem OAI.ReflexiveFixedPoints.OrderedTree.mem_descendants line 108
  18. theorem OAI.ReflexiveFixedPoints.OrderedTree.descendants_nonempty line 113
  19. theorem OAI.ReflexiveFixedPoints.OrderedTree.ancestorLE_eq_of_between line 119

    Source documentation

    Every node between two descendants of the same node is a descendant.

    theorem ancestorLE_eq_of_between {i j : ℕ} (h : i ≤ j) (v : T.Node i)
    {a b c : T.Node j} (hab : a ≤ b) (hbc : b ≤ c)
    (ha : T.ancestorLE h a = v) (hc : T.ancestorLE h c = v) :
    T.ancestorLE h b = v := by
…
  20. theorem OAI.ReflexiveFixedPoints.OrderedTree.mem_descendants_of_between line 127