Simple normal crossings with a clopen part of the centre, and the snc dimension bound

Two facts about an snc family F [Kol07, Definition 24]: F has simple normal crossings with a clopen part Y ∩ O of a set it has simple normal crossings with (the common adapted/snc chart at a point restricted to O), and at most n members of F pass through a point (the snc chart at the point injects the members through it into the n coordinates, [Kol07, Definition 24 (3)]). Placed beside the meet-locus charts (MeetLocusChart.lean), whose IsSncChartAt.restrOpen_of_isOpen restricts the snc chart. Used where a centre is a union of some of the components of an intersection of boundary hypersurfaces (Hironaka/Resolution/Analytic/OrderReduction/BMO/Step3Monomial/Ideal.lean).

theorem Manifold.HypersurfaceFamily.HasSncWith.inter_of_isOpen {𝕜 : 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} {Y : Set M} {c : ℕ} (h : HasSncWith ψ F Y c) {O : Set M} (hO : IsOpen O) : HasSncWith ψ F (Y ∩ O) c

Simple normal crossings with a clopen part of the centre.

theorem Manifold.HypersurfaceFamily.IsSnc.card_le {𝕜 : 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) (x : M) (s : Finset F.ι) (hs : ∀ j ∈ s, x ∈ F.hyp j) : s.card ≤ n

At most n members of an snc family pass through a point ([Kol07, Definition 24 (3)]): the snc chart at the point injects them into the coordinates.