OrderedChainKnots.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Indexed knots of an ordered dyadic chain

An actual consecutive list of dyadic cells covering [0,1] gives a strictly increasing subdivision indexed by that same list. The two endpoints of its ith piece are exactly the endpoints of the ith listed cell.

def OAI.ThompsonNonamenability.GapChain.realKnots line 23
Source documentation
The initial endpoint followed by the right endpoints of the cells.
```
def realKnots : (a : ℝ) → (L : List BasicInterval) → Fin (L.length + 1) → ℝ
  | a, [], _ => a
  | a, I :: L, i => Fin.cases a (realKnots I.right L) i
```
Mentions: OAI.ThompsonNonamenability.BasicInterval
theorem OAI.ThompsonNonamenability.GapChain.realKnots_zero line 27
theorem OAI.ThompsonNonamenability.GapChain.realKnots_succ line 32
Source documentation
The right knot of each indexed piece is its actual right endpoint.
```
theorem realKnots_succ (a : ℝ) (L : List BasicInterval) (i : Fin L.length) :
    realKnots a L i.succ = (L.get i).right := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.GapChain.realKnots
theorem OAI.ThompsonNonamenability.GapChain.realKnots_castSucc line 44
Source documentation
The chain equalities identify each left knot with its listed cell.
```
theorem realKnots_castSucc {a b : ℝ} {L : List BasicInterval}
    (h : GapChain a b L) (i : Fin L.length) :
    realKnots a L i.castSucc = (L.get i).left := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.GapChain, OAI.ThompsonNonamenability.GapChain.realKnots
theorem OAI.ThompsonNonamenability.GapChain.realKnots_last line 56
theorem OAI.ThompsonNonamenability.GapChain.strictMono_realKnots line 64
theorem OAI.ThompsonNonamenability.GapChain.length_pos line 71
theorem OAI.ThompsonNonamenability.GapChain.realKnots_mem_unit line 77
theorem OAI.ThompsonNonamenability.GapChain.isDyadic_realKnots line 85
structure OAI.ThompsonNonamenability.ChainSubdivision line 96
Source documentation
A subdivision whose indexing agrees with an actual ordered cell list.
```
structure ChainSubdivision (L : List BasicInterval) where
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval
def OAI.ThompsonNonamenability.GapChain.toSubdivision line 111
Source documentation
Construct all subdivision data from the chain equalities.
```
def toSubdivision {L : List BasicInterval} (h : GapChain 0 1 L) :
    ChainSubdivision L := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.GapChain, OAI.ThompsonNonamenability.ChainSubdivision
theorem OAI.ThompsonNonamenability.ChainSubdivision.mem_carrier_iff line 137
Source documentation
Membership in an indexed cell is exactly membership between its knots.
```
theorem mem_carrier_iff {L : List BasicInterval} (s : ChainSubdivision L)
    (i : Fin L.length) (x : UnitInterval) :
    (x : ℝ) ∈ (L.get i).carrier ↔ s.knots i.castSucc ≤ x ∧ x ≤ s.knots i.succ := by
…
```
Mentions: OAI.ThompsonNonamenability.BasicInterval, OAI.ThompsonNonamenability.ChainSubdivision, OAI.ThompsonNonamenability.UnitInterval