The complement of a simple normal crossings divisor is dense

The complement of the support of an snc divisor is dense (IsSnc.dense_compl_support): near a point a the support is the union of the components through a (IsSnc.exists_nhds_support_eq, local finiteness), and in an snc chart at a those components are finitely many coordinate hyperplanes (IsSncChartAt, the coordinate indices c injective), whose complement is dense in the model space E (a proper closed subspace of a normed space has empty interior — Mathlib's Submodule.eq_top_of_nonempty_interior'; finitely many, by the Baire property of the finite-dimensional E). This is the density that makes a resolution a modification: Hironaka remarks that the complement of the exceptional set is dense for reduced complex-analytic spaces but not always for real ones [Hir64, p. 111], and Bierstone–Milman ask for Reg X to be Zariski-dense [BM97, Remarks 1.7 (2)]; for the boundary divisor of a resolution the density holds on the nose.

• dense_setOf_coord_ne_zero: the complement of one coordinate hyperplane {ψ z i = 0} of E is dense;
• dense_setOf_forall_coord_ne_zero: the complement of finitely many is dense;
• HypersurfaceFamily.IsSnc.exists_notMem_support_of_mem_nhds: every neighbourhood of a point contains a point off the support;
• HypersurfaceFamily.IsSnc.dense_compl_support: the complement of the support is dense.

It is used to define the set of a simple normal crossings divisor on an analytic space (Hironaka/AnalyticSpace/SncDivisorSetLocal.lean).

theorem Manifold.dense_setOf_coord_ne_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (i : Fin n) : Dense {z : E | ψ z i ≠ 0}

The complement of the coordinate hyperplane {z | ψ z i = 0} of E is dense: the hyperplane is a proper closed subspace, hence has empty interior (Submodule.eq_top_of_nonempty_interior').

theorem Manifold.dense_setOf_forall_coord_ne_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {J : Type u_2} [Finite J] (c : J → Fin n) : Dense {z : E | ∀ (j : J), ψ z (c j) ≠ 0}

The complement of finitely many coordinate hyperplanes of E is dense (E is finite-dimensional, hence complete and a Baire space).

theorem Manifold.HypersurfaceFamily.IsSnc.exists_notMem_support_of_mem_nhds {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} (hF : IsSnc ψ F) {a : M} {N : Set M} (hN : N ∈ nhds a) : ∃ x ∈ N, x ∉ F.support

Every neighbourhood of a point a of the manifold contains a point off the support of an snc divisor: near a the support is the union of the components through a (IsSnc.exists_nhds_support_eq), which in an snc chart at a are finitely many coordinate hyperplanes, and the complement of finitely many coordinate hyperplanes is dense in the model.

theorem Manifold.HypersurfaceFamily.IsSnc.dense_compl_support {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {F : HypersurfaceFamily M} (hF : IsSnc ψ F) : Dense F.supportᶜ

The complement of the support of a simple normal crossings divisor is dense.