instEstimatorPureTrivial — Mathlib

English

There is a natural estimator relation between a pure thunk and a trivial estimator: Estimator (Thunk.pure a) (Estimator.trivial a).

Русский

Существует естественная зависимость оценивателя между чистым отложением и тривиальным оценивателем.

LaTeX

$$Estimator (Thunk.pure a) (Estimator.trivial a)$$

Lean4

instance {a : α} : Estimator (Thunk.pure a) (Estimator.trivial a)
    where
  bound b := b.val
  improve _ := none
  bound_le b := b.prop.le
  improve_spec b := b.prop

Похожие утверждения