finite_of_degree_le — Mathlib

English

If σ is finite, then the set {f : σ →₀ ℕ | deg f ≤ n} is finite.

Русский

Если σ конечно, то множество {f : σ →₀ ℕ | deg f ≤ n} конечно.

LaTeX

$$$\left\{ f : \sigma \to_0 \mathbb{N} \mid \deg f \le n \right\} \\text{ is finite}$$$

Lean4

theorem finite_of_degree_le [Finite σ] (n : ℕ) : {f : σ →₀ ℕ | degree f ≤ n}.Finite :=
  by
  simp_rw [degree_eq_weight_one]
  refine finite_of_nat_weight_le (Function.const σ 1) ?_ n
  intro _
  simp only [Function.const_apply, ne_eq, one_ne_zero, not_false_eq_true]

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