castSucc_castPred — Mathlib

English

CastSucc after castPred recovers the original element; castSucc (i.castPred h) = i.

Русский

CastSucc после castPred восстанавливает исходный элемент; castSucc (i.castPred h) = i.

LaTeX

$$$$ \\@[simp] \\forall {n}: {i : \\mathrm{Fin}(n+1)} (h): \\operatorname{castSucc}(i.castPred\\, h) = i. $$$$

Lean4

@[simp]
theorem castSucc_castPred (i : Fin (n + 1)) (h : i ≠ last n) : castSucc (i.castPred h) = i :=
  by
  rcases exists_castSucc_eq.mpr h with ⟨y, rfl⟩
  rw [castPred_castSucc]

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