theorem bounded_canonical_height_finite {K : Type u_1} [Field K] [NumberField K] (W : WeierstrassCurve K) [W.IsElliptic] (h : W.toAffine.Point → ℝ) (hWeil : IsWeilHeightOnCurve W h) (B : ℝ) : {P : W.toAffine.Point | EllipticCurve.NeronTateHeight W h hWeil P ≤ B}.Finite

Northcott property for the canonical (Néron-Tate) height: the set of points $P \in E(K)$ with $\hat{h}(P) \leq B$ is finite for any bound $B$.