castPred_le_castPred — Mathlib

English

If i ≤ j and j ≠ last n, then castPred(i, hi) ≤ castPred(j, hj).

Русский

Если i ≤ j и j ≠ последний элемент Fin(n), то castPred(i, hi) ≤ castPred(j, hj).

LaTeX

$$$ \operatorname{castPred}(i, h_i) \le \operatorname{castPred}(j, h_j) \quad\text{при условии}\quad i \le j,\ j \neq \mathrm{last}(n). $$$

Lean4

/-- A version of the right-to-left implication of `castPred_le_castPred_iff`
that deduces `i ≠ last n` from `i ≤ j` and `j ≠ last n`. -/
@[gcongr]
theorem castPred_le_castPred {i j : Fin (n + 1)} (h : i ≤ j) (hj : j ≠ last n) :
    castPred i (by rw [← lt_last_iff_ne_last] at hj ⊢; exact Fin.lt_of_le_of_lt h hj) ≤ castPred j hj :=
  h

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