exists_eq_add_of_le — Mathlib

English

If a ≤ b in Fin n, there exists k ≤ b with b = a + k.

Русский

Если a ≤ b в Fin n, существует k ≤ b такой, что b = a + k.

LaTeX

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

Lean4

theorem exists_eq_add_of_le {n : ℕ} {a b : Fin n} (h : a ≤ b) : ∃ k ≤ b, b = a + k :=
  by
  obtain ⟨k, hk⟩ : ∃ k : ℕ, (b : ℕ) = a + k := Nat.exists_eq_add_of_le h
  have hkb : k ≤ b := by omega
  refine ⟨⟨k, hkb.trans_lt b.is_lt⟩, hkb, ?_⟩
  simp [Fin.ext_iff, Fin.val_add, ← hk, Nat.mod_eq_of_lt b.is_lt]

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