pred_le_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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