English
Let q be a divisor in a chain c: Fin(n+1) → Associates(M) with StrictMono c and the chain property: every divisor r ≤ q equals some c(i). Then c(0) is a unit.
Русский
Пусть q является элементом цепи делителей c: Fin(n+1) → Associates(M) с строго возрастающей c и свойством: любой делитель r ≤ q равен некоторому c(i). Тогда c(0) является единицей.
LaTeX
$$$\text{If } c\text{ is StrictMono and } (\forall r,\ r \le q \iff \exists i, r=c(i)),\text{ then } \mathrm{IsUnit}(c(0)).$$$
Lean4
theorem first_of_chain_isUnit {q : Associates M} {n : ℕ} {c : Fin (n + 1) → Associates M} (h₁ : StrictMono c)
(h₂ : ∀ {r}, r ≤ q ↔ ∃ i, r = c i) : IsUnit (c 0) :=
by
obtain ⟨i, hr⟩ := h₂.mp Associates.one_le
rw [Associates.isUnit_iff_eq_one, ← Associates.le_one_iff, hr]
exact h₁.monotone (Fin.zero_le i)
