strictMono_pred_comp — Mathlib

English

Let α be a preorder and f: α → Fin(n+1) with f(a) ≠ 0 for all a. If f is strictly monotone, then a ↦ pred(f(a))(hf(a)) is strictly 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{StrictMono}\ f \rightarrow \mathrm{StrictMono}\ (\lambda a, (f(a)).pred (hf(a)))$$$

Lean4

theorem strictMono_pred_comp (hf : ∀ a, f a ≠ 0) (hf₂ : StrictMono f) : StrictMono (fun a => pred (f a) (hf a)) :=
  fun _ _ h => pred_lt_pred_iff.2 (hf₂ h)

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