strictMono_vecCons — Mathlib

English

Strict monotonicity of vecCons a f holds exactly when a < f(0) and f is strictly monotone.

Русский

Строго монотонное отображение vecCons a f эквивалентно тому, что a < f(0) и f строго монотонна.

LaTeX

$$$\text{StrictMono}(\text{vecCons } a f) \iff a < f(0) \land \text{StrictMono} f.$$$

Lean4

@[simp]
theorem strictMono_vecCons : StrictMono (vecCons a f) ↔ a < f 0 ∧ StrictMono f :=
  liftFun_vecCons (· < ·)

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