castPred_le_castPred_iff — Mathlib

English

For i, j in Fin(n+1) with hi, hj ≠ last n, castPred(i, hi) ≤ castPred(j, hj) if and only if i ≤ j.

Русский

Пусть i, j ∈ Fin(n+1) и hi, hj ≠ last n. Тогда castPred(i, hi) ≤ castPred(j, hj) тогда и только если i ≤ j.

LaTeX

$$$ \operatorname{castPred}(i, h_i) \le \operatorname{castPred}(j, h_j) \iff i \le j. $$$

Lean4

@[simp]
theorem castPred_le_castPred_iff {i j : Fin (n + 1)} {hi : i ≠ last n} {hj : j ≠ last n} :
    castPred i hi ≤ castPred j hj ↔ i ≤ j :=
  Iff.rfl

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