Locally finite countable covers of an analytic space #
An analytic K-space is locally compact (locally a local analytic K-space, clause (i) of the
definition in [Hir64, Ch. 0, §1, p. 120]), countable at infinity (clause (ii)) and Hausdorff
(clause (iii)), hence paracompact. If a property P of open subspaces is stable under passing to
smaller open subsets and holds on a neighbourhood of every point, then X has a
countable, locally finite open cover by open subsets with compact closures on which P holds
(exists_locallyFinite_cover). This is the cover the gluing of local complexifications starts from,
with P the property of admitting an analytic complexification (stable under restriction by
Complexification.restrictLe, Hironaka.AnalyticSpace.Glue.Restrict); it is the locally finite
cover of the proof of [BW59, Proposition 1], and the pair of locally finite covers V̄_i ⊆ U_i of
the proof of [Car57, §3, Proposition 2].
Conventions. The cover is indexed by a type ι : Type u with Countable ι; empty members are
excluded, so that the countability comes from the local finiteness in a σ-compact space (Mathlib's
LocallyFinite.countable_univ). The refinement is Mathlib's precise_refinement on the cover by
the neighbourhoods U x ∩ K x, K x an open neighbourhood of x with compact closure. For X = ∅
the index type is empty and every clause holds trivially; for X compact the cover is finite; for
P trivially true one gets a locally finite countable cover by relatively compact open subsets.
A locally finite countable open cover of an analytic space by relatively compact opens on which a restriction-stable local property holds.