monotone_castPred_comp — Mathlib

English

If hf(a) ensures f(a) ≠ last n and f is monotone, then the map a ↦ castPred(f(a)) (hf(a)) is monotone.

Русский

Если hf(a) обеспечивает, что f(a) ≠ last n и f монотонен, то отображение a ↦ castPred(f(a)) (hf(a)) монотонно.

LaTeX

$$$(\forall a, f(a) \neq \mathrm{last}\ n) \to \mathrm{Monotone}(f) \to \mathrm{Monotone}(a \mapsto \mathrm{castPred}(f(a))(hf(a)))$$$

Lean4

theorem monotone_castPred_comp (hf : ∀ a, f a ≠ last n) (hf₂ : Monotone f) :
    Monotone (fun a => castPred (f a) (hf a)) := fun _ _ h => castPred_le_castPred_iff.2 (hf₂ h)

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