Residual points form a well-ordered set #
Berarducci, Remark 6.3: the translated truncation b^{|γ} lies in J unless γ belongs to the
order-topological closure of the support of b, so it is nonzero modulo J only for γ ranging
over a well-ordered set. Since a residual point has translated truncation of nonzero ordinal
value, the residual-point set is contained in that closure and is therefore partially well
ordered.
The two inputs are the vanishing of a germ outside the closed support, which is an elementary metric argument, and the fact that the closure of a partially well-ordered set of reals is again partially well ordered.
theorem
Berarducci.residualPointSet_subset_closure_support
{K : Type v}
[Field K]
(b : SeriesWithOrdinalValueAboveOne K)
:
residualPointSet b ⊆ closure (↑↑b).support
Residual points lie in the closure of the support.
theorem
Berarducci.residualPointSet_isPWO
{K : Type v}
[Field K]
(b : SeriesWithOrdinalValueAboveOne K)
:
Berarducci, Remark 6.3: the residual-point set is partially well ordered.