vecCons — Mathlib

English

If f is strictly monotone and a is strictly smaller than the first value f(0), then the vector obtained by prepending a to f, vecCons a f, is strictly monotone.

Русский

Если f строго монотонна и a меньше, чем первое значение f(0), тогда vecCons a f является строго монотонной.

LaTeX

$$$\text{StrictMono}(\mathrm{vecCons}(a,f))\;\text{if}\; \text{StrictMono}(f) \text{ and } a < f(0)$$$

Lean4

theorem vecCons (hf : StrictMono f) (ha : a < f 0) : StrictMono (vecCons a f) :=
  strictMono_vecCons.2 ⟨ha, hf⟩

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