coprimes_lt — Mathlib

English

For a function a: Fin m → ℕ, each component a(i) is strictly less than the corresponding bound coprimes a i.

Русский

Для функции a: Fin(m) → ℕ каждое место i удовлетворяет неравенству a(i) < coprimes(a,i).

LaTeX

$$$a(i) < \\operatorname{coprimes}(a,i)$ for all i ∈ Fin(m)$$

Lean4

theorem coprimes_lt (a : Fin m → ℕ) (i) : a i < coprimes a i :=
  by
  have h₁ : a i < supOfSeq a := Nat.lt_add_one_iff.mpr (le_max_of_le_right <| Finset.le_sup (by simp))
  have h₂ : supOfSeq a ≤ (i + 1) * (supOfSeq a)! + 1 :=
    le_trans (self_le_factorial _) (le_trans (Nat.le_mul_of_pos_left (supOfSeq a)! (succ_pos i)) (le_add_right _ _))
  simpa only [coprimes] using lt_of_lt_of_le h₁ h₂

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