monotone_pred_comp — Mathlib

English

Let α be a preorder and f: α → Fin(n+1) with f(a) ≠ 0 for all a. If f is monotone, then a ↦ pred(f(a))(hf(a)) is monotone.

Русский

Пусть A упорядочено и f: A → Fin(n+1) таково, что f(a) ≠ 0 для всех a. Если f монотоно, то a ↦ pred(f(a))(hf(a)) монотоном.

LaTeX

$$$\forall {n} {\alpha} [\mathrm{Preorder}] {f : \alpha \to \mathrm{Fin}(n+1)} (hf : \forall a, f(a) \neq 0),\ \mathrm{Monotone}\ f \rightarrow \mathrm{Monotone}\ (\lambda a, (f(a)).pred (hf(a)))$$$

Lean4

theorem monotone_pred_comp (hf : ∀ a, f a ≠ 0) (hf₂ : Monotone f) : Monotone (fun a => pred (f a) (hf a)) :=
  fun _ _ h => pred_le_pred_iff.2 (hf₂ h)

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