monotone_vecCons — Mathlib

English

Monotonicity of vecCons a f is equivalent to a ≤ f(0) and f is monotone.

Русский

Монотонность vecCons a f эквивалентна неравенству a ≤ f(0) и монотонности f.

LaTeX

$$$\text{Monotone}(\text{vecCons } a f) \iff a \le f(0) \land \text{Monotone} f.$$$

Lean4

@[simp]
theorem monotone_vecCons : Monotone (vecCons a f) ↔ a ≤ f 0 ∧ Monotone f := by
  simpa only [monotone_iff_forall_lt] using @liftFun_vecCons α n (· ≤ ·) _ f a

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