A sub-family of a simple normal crossing family is snc #
The conditions (1)–(4) of [Kol07, Definition 24] concern each member and the members through a
point; selecting members (subfamily of Hironaka.Scheme.Snc.SncOn) keeps them — the injective
inclusion of the selected members preserves the components (isSncAt_of_injective_components of
Hironaka.Resolution.Algebraic.Snc.SncOnTransport). Used for the exceptional sub-family F_r of
E_r as the boundary of the triple of [Kol07, Theorem 92], and by
Hironaka.Resolution.Algebraic.Kol07.UnionIdealInvertible.
Source: [Kol07, Definition 24].
theorem
AlgebraicGeometry.Scheme.DivisorFamily.IsSnc.subfamily
{X : Scheme}
{E : X.DivisorFamily}
(hE : E.IsSnc)
(p : E.ι → Prop)
:
A sub-family of an snc family is snc [Kol07, Definition 24].