castPred_eq_iff_eq_castSucc — Mathlib

English

Let i be an element of Fin(n+1) with i ≠ last n, and j an element of Fin n. Then castPred(i, hi) = j if and only if i = castSucc(j).

Русский

Пусть i ∈ Fin(n+1) и i ≠ последнее элемент Fin(n); пусть j ∈ Fin n. Тогда castPred(i, hi) = j тогда же, если и только если i = castSucc(j).

LaTeX

$$$ \operatorname{castPred}(i, h_i) = j \iff i = \operatorname{castSucc}(j). $$$

Lean4

theorem castPred_eq_iff_eq_castSucc (i : Fin (n + 1)) (hi : i ≠ last _) (j : Fin n) :
    castPred i hi = j ↔ i = castSucc j :=
  ⟨fun h => by rw [← h, castSucc_castPred], fun h => by simp_rw [h, castPred_castSucc]⟩

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