lt_pred_iff — Mathlib

English

For j ∈ Fin n and i ∈ Fin(n+1) with i ≠ 0, j < pred i hi iff succ j < i.

Русский

Для j ∈ Fin(n) и i ∈ Fin(n+1) с i ≠ 0: j < pred i hi ⇔ succ j < i.

LaTeX

$$$$ \\forall {j \\in \\mathrm{Fin}(n)}, {i \\in \\mathrm{Fin}(n+1)} (hi: i \\neq 0): j < \\operatorname{pred}(i, hi) \\iff \\operatorname{succ}(j) < i. $$$$

Lean4

theorem lt_pred_iff {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) : j < pred i hi ↔ succ j < i := by
  rw [← succ_lt_succ_iff, succ_pred]

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