OrderedTreeIntervals.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Consecutive descendant blocks in an ordered tree

The ancestor maps are monotone and surjective. Their nonempty fibers are intervals. Endpoints are natural numbers, so the upper endpoint may equal the cardinality of the terminal level.

def OAI.ReflexiveFixedPoints.OrderedTree.descendantFirst line 19
Source documentation
The first terminal-level descendant.
```
noncomputable def descendantFirst (h : i ≤ j) (v : T.Node i) : T.Node j :=
…
```
def OAI.ReflexiveFixedPoints.OrderedTree.descendantLast line 23
Source documentation
The last terminal-level descendant.
```
noncomputable def descendantLast (h : i ≤ j) (v : T.Node i) : T.Node j :=
…
```
def OAI.ReflexiveFixedPoints.OrderedTree.descendantLo line 27
Source documentation
Inclusive lower endpoint of the descendant block.
```
noncomputable def descendantLo (h : i ≤ j) (v : T.Node i) : ℕ :=
…
```
def OAI.ReflexiveFixedPoints.OrderedTree.descendantHi line 31
Source documentation
Exclusive upper endpoint of the descendant block.
```
noncomputable def descendantHi (h : i ≤ j) (v : T.Node i) : ℕ :=
…
```
theorem OAI.ReflexiveFixedPoints.OrderedTree.ancestorLE_descendantFirst line 35
theorem OAI.ReflexiveFixedPoints.OrderedTree.ancestorLE_descendantLast line 41
theorem OAI.ReflexiveFixedPoints.OrderedTree.descendantFirst_le_of_ancestor_eq line 46
theorem OAI.ReflexiveFixedPoints.OrderedTree.le_descendantLast_of_ancestor_eq line 52
theorem OAI.ReflexiveFixedPoints.OrderedTree.ancestorLE_eq_iff_interval line 60
Source documentation
An ancestor fiber is exactly the natural half-open interval between its first descendant and one past its last descendant.
```
theorem ancestorLE_eq_iff_interval (h : i ≤ j) (v : T.Node i) (s : T.Node j) :
    T.ancestorLE h s = v ↔
      T.descendantLo h v ≤ s.val ∧ s.val < T.descendantHi h v := by
…
```
theorem OAI.ReflexiveFixedPoints.OrderedTree.descendantLo_lt_hi line 85
theorem OAI.ReflexiveFixedPoints.OrderedTree.descendantHi_le_size line 91
theorem OAI.ReflexiveFixedPoints.OrderedTree.descendantLo_lt_size line 95
theorem OAI.ReflexiveFixedPoints.OrderedTree.descendantHi_le_descendantLo_of_lt line 100
Source documentation
Earlier nodes have descendant blocks entirely before later nodes' blocks.
```
theorem descendantHi_le_descendantLo_of_lt (h : i ≤ j)
    (v w : T.Node i) (hvw : v < w) :
    T.descendantHi h v ≤ T.descendantLo h w := by
…
```

theorem OAI.ReflexiveFixedPoints.OrderedTree.self_mem_ancestor_interval line 117

Source documentation

Every leaf belongs to its own ancestor's block.

theorem self_mem_ancestor_interval (h : i ≤ j) (s : T.Node j) :
    T.descendantLo h (T.ancestorLE h s) ≤ s.val ∧
      s.val < T.descendantHi h (T.ancestorLE h s) :=
…

theorem OAI.ReflexiveFixedPoints.OrderedTree.lt_descendantLo_iff_ancestorLE_lt line 124
Source documentation
The threshold at the start of v's block separates precisely the nodes whose ancestor lies strictly before v.
```
theorem lt_descendantLo_iff_ancestorLE_lt (h : i ≤ j)
    (v : T.Node i) (s : T.Node j) :
    s.val < T.descendantLo h v ↔ T.ancestorLE h s < v := by
…
```
theorem OAI.ReflexiveFixedPoints.OrderedTree.lt_descendantHi_iff_ancestorLE_le line 148
Source documentation
The threshold just after the end of v's block separates exactly the nodes whose ancestor is at most v.
```
theorem lt_descendantHi_iff_ancestorLE_le (h : i ≤ j)
    (v : T.Node i) (s : T.Node j) :
    s.val < T.descendantHi h v ↔ T.ancestorLE h s ≤ v := by
…
```