le_pred_castSucc_iff — Mathlib

English

For a and b in Fin(n+1) with castSucc a ≠ 0, b ≤ (castSucc a).pred ha holds iff b < a.

Русский

Для a,b ∈ Fin(n+1) с castSucc a ≠ 0: b ≤ (castSucc a).pred ha эквивалентно b < a.

LaTeX

$$$$ \\forall {a,b} \\in \\mathrm{Fin}(n+1) (ha: castSucc(a) \\neq 0): b \\le (\\operatorname{castSucc}(a)).pred ha \\iff b < a. $$$$

Lean4

theorem le_pred_castSucc_iff {a b : Fin (n + 1)} (ha : castSucc a ≠ 0) : b ≤ (castSucc a).pred ha ↔ b < a := by
  rw [le_pred_iff, succ_le_castSucc_iff]

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