English
Let α be a preordered set and f : α → Fin(n+1) be strictly increasing and never equal to the top element Fin.last n. Then the function a ↦ castPred (f(a)) (hf a) is strictly increasing, i.e. preserves the strict order.
Русский
Пусть α имеет предикорный порядок и f : α → Fin(n+1) строго возрастает и нигде не достигает максимального элемента Fin.last n. Тогда отображение a ↦ castPred (f(a)) (hf a) строго возрастает по порядку.
LaTeX
$$$\\forall f:\\mathcal{A}\\to \\mathrm{Fin}(n+1),\\ (\\forall a, f(a) \\neq \\mathrm{Fin.last}\,n) \\wedge \\mathrm{StrictMono} f \\Rightarrow \\mathrm{StrictMono}\\bigl(a \\mapsto \\mathrm{castPred}(f(a))\\bigr).$$$
Lean4
theorem strictMono_castPred_comp (hf : ∀ a, f a ≠ last n) (hf₂ : StrictMono f) :
StrictMono (fun a => castPred (f a) (hf a)) := fun _ _ h => castPred_lt_castPred_iff.2 (hf₂ h)
