SortedSubdivision.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Sorting finite subdivisions of the unit interval

Sorting a finite set containing the endpoints produces a genuine subdivision. If that set also contains the knots of an earlier subdivision, every new closed piece is contained in an old closed piece.

structure OAI.ThompsonNonamenability.SortedSubdivision line 17
theorem OAI.ThompsonNonamenability.SortedSubdivision.cover_of_endpoints line 33
Source documentation
The adjacent closed intervals cover the unit interval. Monotonicity is not needed for this auxiliary fact: take the last left endpoint below the point.
```
theorem cover_of_endpoints {n : ℕ} (hn : 0 < n)
    (knots : Fin (n + 1) → UnitInterval)
    (hfirst : knots 0 = unitIntervalZero)
    (hlast : knots (Fin.last n) = unitIntervalOne) (x : UnitInterval) :
    ∃ i : Fin n, knots i.castSucc ≤ x ∧ x ≤ knots i.succ := by
…
```
Mentions: OAI.ThompsonNonamenability.UnitInterval, OAI.ThompsonNonamenability.unitIntervalZero, OAI.ThompsonNonamenability.unitIntervalOne
def OAI.ThompsonNonamenability.SortedSubdivision.ofFinset line 72
Source documentation
Increasing enumeration of the actual finite knot set.
```
noncomputable def ofFinset (S : Finset UnitInterval)
    (h0 : unitIntervalZero ∈ S) (h1 : unitIntervalOne ∈ S) :
    SortedSubdivision S := by
…
```
Mentions: OAI.ThompsonNonamenability.UnitInterval, OAI.ThompsonNonamenability.unitIntervalZero, OAI.ThompsonNonamenability.unitIntervalOne, OAI.ThompsonNonamenability.SortedSubdivision
theorem OAI.ThompsonNonamenability.SortedSubdivision.no_mem_between line 116
Source documentation
No point of the sorted knot set lies strictly between successive knots.
```
theorem no_mem_between {S : Finset UnitInterval} (r : SortedSubdivision S)
    (i : Fin r.pieceCount) {x : UnitInterval} (hx : x ∈ S) :
    ¬ (r.knots i.castSucc < x ∧ x < r.knots i.succ) := by
…
```
Mentions: OAI.ThompsonNonamenability.UnitInterval, OAI.ThompsonNonamenability.SortedSubdivision

theorem OAI.ThompsonNonamenability.SortedSubdivision.adjacent_contained line 130

Source documentation

A refinement containing every original knot has each closed piece inside one original closed piece. The interior point selects a piece even when a refined endpoint is itself an original knot.

theorem adjacent_contained {S : Finset UnitInterval} (r : SortedSubdivision S)
    {n : ℕ} (old : Fin (n + 1) → UnitInterval) (_hold : StrictMono old)
    (hcover : ∀ x : UnitInterval, ∃ j : Fin n,
      old j.castSucc ≤ x ∧ x ≤ old j.succ)
    (hmem : ∀ j, old j ∈ S) (i : Fin r.pieceCount) :
    ∃ j : Fin n, old j.castSucc ≤ r.knots i.castSucc ∧
      r.knots i.succ ≤ old j.succ := by
…

Mentions: OAI.ThompsonNonamenability.UnitInterval, OAI.ThompsonNonamenability.SortedSubdivision