coe_succ_lt_iff_lt — Mathlib

English

For any n and j,k in Fin(n), the inequality (j cast to Fin(n+1)) < k holds if and only if j < k.

Русский

Для любых j,k ∈ Fin(n) верно: (j в Fin(n+1)) < k тогда и только тогда, когда j < k.

LaTeX

$$$$ \\forall n \\in \\mathbb{N}, \\forall j,k \\in \\mathrm{Fin}(n): (j \\uparrow \\mathrm{to\\,Fin}(n+1)) < k \\iff j < k. $$$$

Lean4

theorem coe_succ_lt_iff_lt {n : ℕ} {j k : Fin n} : (j : Fin (n + 1)) < k ↔ j < k := by
  simp only [coe_eq_castSucc, castSucc_lt_castSucc_iff]

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