castPred_lt_castPred — Mathlib

English

If i < j, then castPred(i, hi) < castPred(j, hj).

Русский

Если i < j, то castPred(i, hi) < castPred(j, hj).

LaTeX

$$$ i < j \quad\Rightarrow\quad \operatorname{castPred}(i, h_i) < \operatorname{castPred}(j, h_j). $$$

Lean4

/-- A version of the right-to-left implication of `castPred_lt_castPred_iff`
that deduces `i ≠ last n` from `i < j`. -/
@[gcongr]
theorem castPred_lt_castPred {i j : Fin (n + 1)} (h : i < j) (hj : j ≠ last n) :
    castPred i (ne_last_of_lt h) < castPred j hj :=
  h

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