English
An LTSeries can be constructed from a length, a function Fin(length+1) → α, and a StrictMono toFun.
Русский
LTSeries строится из длины, функции Fin(length+1) → α и StrictMono к функции toFun.
LaTeX
$$$\text{@[simps]}\text{ def mk (length : }\mathbb{N}\text{) (toFun : Fin (length + 1) → α) (strictMono : StrictMono toFun) : LTSeries α}$$$
Lean4
/-- An alternative constructor of `LTSeries` from a strictly monotone function. -/
@[simps]
def mk (length : ℕ) (toFun : Fin (length + 1) → α) (strictMono : StrictMono toFun) : LTSeries α
where
length := length
toFun := toFun
step i := strictMono <| lt_add_one i.1
