pred_castSucc_lt_iff — Mathlib

English

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

Русский

Для a,b ∈ Fin(n+1) с ha ≠ 0: (castSucc a).pred ha < b ⇔ a ≤ b.

LaTeX

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

Lean4

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

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