exists_eq_add_of_lt — Mathlib

English

If a < b in Fin(n+1), there exists k with k < b and b = a + k + 1.

Русский

Если a < b в Fin(n+1), существует k < b и b = a + k + 1.

LaTeX

$$$\\forall {n} {a,b : \\mathrm{Fin}(n+1)}, a < b \\Rightarrow \\exists k < b, k + 1 \\le b \\land b = a + k + 1$$$

Lean4

theorem exists_eq_add_of_lt {n : ℕ} {a b : Fin (n + 1)} (h : a < b) : ∃ k < b, k + 1 ≤ b ∧ b = a + k + 1 :=
  by
  cases n
  · cutsat
  obtain ⟨k, hk⟩ : ∃ k : ℕ, (b : ℕ) = a + k + 1 := Nat.exists_eq_add_of_lt h
  have hkb : k < b := by omega
  refine ⟨⟨k, hkb.trans b.is_lt⟩, hkb, by fin_omega, ?_⟩
  simp [Fin.ext_iff, Fin.val_add, ← hk, Nat.mod_eq_of_lt b.is_lt]

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