The empty boundary is a simple normal crossing divisor

[Kol07, Notation 64 (3)] asks the boundary E = (E^1, …, E^s) of a triple to be a simple normal crossing divisor; for s = 0 (the triple (𝔸⁴, I, ∅) of [Kol07, Example 106], for instance) the two clauses of [Kol07, Definition 24] are vacuous except for the regular system of parameters at each point, which a smooth k-scheme has (exists_fin_span_eq_maximalIdeal_stalk). Both the family DivisorFamily.empty X and any family with an empty index type are covered.

theorem AlgebraicGeometry.isSnc_empty_of_smooth {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [Smooth f] : (Scheme.DivisorFamily.empty X).IsSnc

On a smooth k-scheme the empty boundary DivisorFamily.empty X is a simple normal crossing divisor [Kol07, Definition 24]: no component to be regular, and at each point the regular system of parameters of the stalk with the empty assignment.

theorem AlgebraicGeometry.isSnc_of_isEmpty {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [Smooth f] (E : X.DivisorFamily) (hE : IsEmpty E.ι) : E.IsSnc

isSnc_empty_of_smooth for ANY divisor family with an empty index type: no component to be regular, and at each point the regular system of parameters of the stalk with the empty assignment. Used for the restricted family E.comap j of a closed-embedding situation with E = ∅ (clause (5) of AlgebraicGeometry.exists_functorial_principalization).