Partitions of the unit interval

unitInterval.Partition n is a monotone sequence 0 = t₀ ≤ ⋯ ≤ tₙ = 1 in the unit interval. It indexes the segments of the tube neighbourhoods of paths in TauCeti.Topology.Homotopy.TubeNeighborhood.

structure unitInterval.Partition (n : ℕ) : Type

A partition 0 = t₀ ≤ ⋯ ≤ tₙ = 1 of the unit interval into n segments.

• t : Fin (n + 1) → ↑unitInterval

  The partition points.

• mono : Monotone self.t

  The partition points are monotone.

• t_zero : self.t 0 = 0

  The first partition point is 0.

• t_last : self.t (Fin.last n) = 1

  The last partition point is 1.

instance unitInterval.Partition.instIsEmptyOfNatNat : IsEmpty (Partition 0)

There is no partition into zero segments, since t 0 would be both 0 and 1.

theorem unitInterval.Partition.t_castSucc_le_succ {n : ℕ} (part : Partition n) (i : Fin n) : part.t i.castSucc ≤ part.t i.succ

Consecutive partition points are ordered.