The generic points of a closed set: a restatement

mem_genericPoints_iff: the generic points of a closed set are the points whose closure is a maximal irreducible subset of it; this restates Closeds.mem_genericPoints_iff of Hironaka/Scheme/IdealSheaf/Order/Along.lean and has no user.

The mathematics of the order function at a point, along a closed subset and under isomorphisms, open immersions and completion is in Hironaka/Scheme/IdealSheaf/Order/Basic.lean, Hironaka/Scheme/IdealSheaf/Order/Along.lean and Hironaka/Scheme/IdealSheaf/Order/Invariance.lean.

theorem AlgebraicGeometry.mem_genericPoints_iff {X : Scheme} (Z : TopologicalSpace.Closeds ↥X) (η : ↥X) : η ∈ Z.genericPoints ↔ Maximal (fun (T : Set ↥X) => T ⊆ ↑Z ∧ IsIrreducible T) (closure {η})

The generic points of a closed set are the points whose closure is a maximal irreducible subset of it; restates Closeds.mem_genericPoints_iff.