Simple points are manifold points; the simple points form an open set

Hironaka [Hir64, Ch. 0, §1, p. 121]: a point x of an analytic K-space X is simple (𝒪_{X,x} regular) iff some open neighbourhood X|V is K-isomorphic to a local analytic K-space (G', 𝒜_{G'}), G' ⊆ K^d open — here with d = dim 𝒪_{X,x} (isRegular_stalk_iff_exists_manifold_nhd). Hironaka has it "by means of jacobian criterion and the implicit function theorem"; the argument here: the easy half is isRegularLocalRing_stalk_of_kIso_analyticSpaceOfOpen (Hironaka/AnalyticSpace/RegularStalk.lean). For the other, the local-model clause of AnalyticSpace gives X|U ≅ (local model)|W with x ↦ w; regularity passes to the stalk of the model at z = w, where the Jacobian criterion hands over c germs generating 𝓘_z with independent differentials (exists_span_eq_of_isRegularLocalRing_stalk, Hironaka/AnalyticSpace/Jacobian.lean), the implicit function theorem gives (model)|V₁ ≅ (G', 𝒜_{G'}) with G' ⊆ K^{n−c} (exists_kIso_analyticSpaceOfOpen_of_span_germ_eq, Hironaka/AnalyticSpace/ModelIso.lean), and the isomorphisms are carried back to an open V' ∋ x of X through Hironaka/AnalyticSpace/Glue.lean. Hence X.regularLocus is open (isOpen_reg), every point of the neighbourhood V being simple, and X.singularLocus = (X.regularLocus)ᶜ is closed (isClosed_singularLocus) — "the open subspace of X which consists of the simple points of X" [Hir64, Introduction].

theorem AnalyticSpace.isRegular_stalk_iff_exists_manifold_nhd {K : Type} [RCLike K] (X : AnalyticSpace K) (x : ↑↑X.toPresheafedSpace) : x ∈ X.regularLocus ↔ ∃ (d : ℕ), ringKrullDim ↑(X.presheaf.stalk x) = ↑d ∧ ∃ (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (_ : x ∈ V) (G' : TopologicalSpace.Opens (Kn K d)), Nonempty ((X.restrictOpen V).KIso (analyticSpaceOfOpen K d G'))

A point is simple iff it has a manifold neighbourhood [Hir64, Ch. 0, §1, p. 121]: x is a simple point of the analytic K-space X iff, for d = dim 𝒪_{X,x}, some open neighbourhood X|V of x is K-isomorphic to a local analytic K-space (G', 𝒜_{G'}) with G' ⊆ K^d open.

theorem AnalyticSpace.isOpen_reg {K : Type} [RCLike K] (X : AnalyticSpace K) : IsOpen X.regularLocus

The simple points form an open set ("the open subspace of X which consists of the simple points" [Hir64, Introduction]).

theorem AnalyticSpace.isClosed_singularLocus {K : Type} [RCLike K] (X : AnalyticSpace K) : IsClosed X.singularLocus

The multiple points form a closed set.