English
If σ is finite and w : σ → ℕ assigns nonzero weights, then the set of d with weight w d ≤ n is finite.
Русский
Если σ конечно, а весовая функция w : σ → ℕ принимает ненулевые значения, то множество d с weight w d ≤ n конечно.
LaTeX
$$ {d : σ →₀ ℕ | weight w d ≤ n}.Finite$$
Lean4
theorem finite_of_nat_weight_le [Finite σ] (w : σ → ℕ) (hw : ∀ x, w x ≠ 0) (n : ℕ) :
{d : σ →₀ ℕ | weight w d ≤ n}.Finite := by
classical
set fg := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n)) with hfg
suffices {d : σ →₀ ℕ | weight w d ≤ n} ⊆ ↑(fg.image fun uv => uv.fst) by
exact Set.Finite.subset (Finset.finite_toSet _) this
intro d hd
rw [hfg]
simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, Finset.mem_antidiagonal, Prod.exists, exists_and_right,
exists_eq_right]
use Finsupp.equivFunOnFinite.symm (Function.const σ n) - d
ext x
simp only [Finsupp.coe_add, Finsupp.coe_tsub, Pi.add_apply, Pi.sub_apply, Finsupp.equivFunOnFinite_symm_apply_toFun,
Function.const_apply]
rw [add_comm]
apply Nat.sub_add_cancel
apply le_trans (le_weight w (hw x) d)
simpa only [Set.mem_setOf_eq] using hd
