pred_lt_iff — Mathlib

English

For j ∈ Fin(n), i ∈ Fin(n+1) with i ≠ 0, the inequality pred i hi < j is equivalent to i < succ j.

Русский

Для j ∈ Fin(n) и i ∈ Fin(n+1) с i ≠ 0 верно: pred i hi < j эквивалентно i < succ j.

LaTeX

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

Lean4

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

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