Lemma 102 in the compatible-family form: the value at an empty member

At an empty member E^j = ∅ the value of BD_{n,m,j} on every relatively compact open is the empty sequence (BDanFam_eq_nil_of_hyp_eq_empty; the counterpart of BDan_eq_nil_of_hyp_eq_empty of BDLemmas.lean). The centre Z_{-1} ⊆ E^j is empty, so its restriction to U is empty and the first blow-up is deleted ([Kol07, 32]); the transform S_0 = π_{-1}^{-1}(E^j) is empty, so the value of the input family on any open of it is a sequence without centres on an empty manifold, hence the empty sequence, and so are its push-forward and its pull-back along the lift.

This is the hypothesis on the data that the commutation of Steps 2.1 and 2.2 with local analytic isomorphisms requires of Lemma 102's family (hnil in LocalFunctorFam.lean), discharged for the family built from the marked families in BOanFamOfInput.lean (bdanFamDataOfInput_fam_eq_nil_of_hyp_eq_empty).

theorem Hironaka.Manifold.BDanFam_eq_nil_of_hyp_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {m : ℕ} (inp : BMOanFam 𝕜 (n - 1) (IsLocalRing.tuningParam m)) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass m T) (j : T.F.ι) (hj : T.F.hyp j = ∅) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : BDanFam m inp T hT j U hU = AnalyticManifold.BlowUpSequence.nil (M.restrict U)

At an empty member the value of BD_{n,m,j} on every relatively compact open is the empty sequence ([Kol07, 32]): the centre Z_{-1} ∩ U is empty and deleted, and the transform S_0 of E^j is empty, so the input family's value on it has no centres.