English
Let q ∈ Associates(M) and c: Fin(n+1) → Associates(M) with the chain property mapping r ≤ q to r = c(i). For every Finset m of Associates(M) with all elements ≤ q, its cardinality is at most n+1.
Русский
Пусть q ∈ Associates(M) и c: Fin(n+1) → Associates(M) задаёт цепь так, что каждый r ≤ q равен некоторому c(i). Тогда для любого Finset m ⊆ Associates(M), все элементы которого удовлетворяют r ≤ q, выполняется |m| ≤ n+1.
LaTeX
$$$(\forall m:\ Finset(\mathrm{Associates}(M)),\ (\forall r\in m, r\le q)\Rightarrow |m| \le n+1)$ при условии $\forall {r},\ r \le q \iff \exists i, r=c(i)$.$$
Lean4
theorem card_subset_divisors_le_length_of_chain {q : Associates M} {n : ℕ} {c : Fin (n + 1) → Associates M}
(h₂ : ∀ {r}, r ≤ q ↔ ∃ i, r = c i) {m : Finset (Associates M)} (hm : ∀ r, r ∈ m → r ≤ q) : m.card ≤ n + 1 := by
classical
have mem_image : ∀ r : Associates M, r ≤ q → r ∈ Finset.univ.image c :=
by
intro r hr
obtain ⟨i, hi⟩ := h₂.1 hr
exact Finset.mem_image.2 ⟨i, Finset.mem_univ _, hi.symm⟩
rw [← Finset.card_fin (n + 1)]
exact (Finset.card_le_card fun x hx => mem_image x <| hm x hx).trans Finset.card_image_le
