theorem finite_nonneg_bounded_of_pd {B : Type u_1} [Fintype B] (f : (B → ℝ) → (B → ℝ) → ℝ) (C c : ℝ) (hc : 0 < c) (hcoerce : ∀ (v : B → ℝ), c * ∑ b : B, v b ^ 2 ≤ f v v) (S : Set (B → ℝ)) (hS_nn : ∀ α ∈ S, ∀ (b : B), 0 ≤ α b) (hS_bdd : ∀ α ∈ S, f α α ≤ C) (hS_discrete : ∀ (b : B), ∀ α ∈ S, ∃ (n : ℤ), α b = ↑n) : S.Finite

Lattice finiteness lemma: a set of integral nonnegative vectors $S \subseteq \mathbb Z_{\ge 0}^B$ with $f(\alpha, \alpha) \le C$ is finite, provided $f$ is coercive ($c\|v\|^2 \le f(v,v)$). This is the abstract finiteness principle underlying the finiteness of root systems on hyperplanes.