The non-original members of the boundary family are finitely many

Along a finite succession the boundary family totalTransformSeqFrom F gains one member per stage (the exceptional divisor, [Kol07, Definition 25]); the members that are not transforms of the original ones (originalIdx) are therefore finitely many. This is the finiteness clause required of the boundary of the disjoined triple of [Kol07, 72], whose boundary is the total transform of finitely many components with the original members collapsed into one (Collapse.lean, DisjoinInput.lean).

theorem AnalyticManifold.FiniteSuccession.finite_setOf_notMem_range_originalIdxAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) (k : ℕ) (h : k < S.length + 1) : {x : (S.totalTransformSeqFromAux F k h).ι | x ∉ Set.range (S.originalIdxAux F k h)}.Finite

The non-original members of the boundary family at stage k form a finite set: none at stage 0, and at stage k + 1 the exceptional divisor together with the images of the non-original members of stage k.

theorem AnalyticManifold.FiniteSuccession.finite_notMem_range_originalIdx {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (F : Manifold.HypersurfaceFamily M.carrier) (i : Fin (S.length + 1)) : Finite { x : (S.totalTransformSeqFrom F i).ι // x ∉ Set.range (S.originalIdx F i) }

The non-original members of the boundary family at stage i are finitely many.