Finitely many étale neighbourhoods cover the closed set

Kollár: "The images of finitely many of the U(p) cover X" ([Kol07, 95], the proof of Theorem 92). Read on the relevant closed set S, for a family of étale neighbourhood pairs Q p : EtaleNbhdPair X p (Hironaka/Scheme/Smooth/Graph.lean) given at the closed points p of S:

• the image of the open V p ⊆ W_p under the étale ψ_p is open (étale morphisms are universally open, Mathlib's UniversallyOpen.of_flat) and contains p (mem_range_ι_comp_ψ);
• for X locally of finite type over a field, X is Jacobson (LocallyOfFiniteType.jacobsonSpace), so these images, over the closed points p of the closed set S, cover S (subset_iUnion_range_ι_comp_ψ, …ψ'; the topology is Hironaka/Algebra/Util/JacobsonCover.lean: every point of S specializes to a closed point of S);
• for X quasi-compact, finitely many closed points suffice, and one finite set serves both families of images by covering with the intersections ψ_p(V p) ∩ ψ'_p(V p) (exists_finset_subset_biUnion_range).

The finite family is assembled into one étale pair on a disjoint union in Hironaka/Resolution/Algebraic/MaximalContact/EtaleEquivSigma.lean.

theorem AlgebraicGeometry.mem_range_ι_comp_ψ {X : Scheme} {p : ↥X} (Q : EtaleNbhdPair X p) {V : Q.W.Opens} (hV : Q.q ∈ V) : p ∈ Set.range ⇑(CategoryTheory.CategoryStruct.comp V.ι Q.ψ)

The point p lies in the image of the open V ∋ q under ψ.

theorem AlgebraicGeometry.mem_range_ι_comp_ψ' {X : Scheme} {p : ↥X} (Q : EtaleNbhdPair X p) {V : Q.W.Opens} (hV : Q.q ∈ V) : p ∈ Set.range ⇑(CategoryTheory.CategoryStruct.comp V.ι Q.ψ')

The point p lies in the image of the open V ∋ q under ψ'.

theorem AlgebraicGeometry.subset_iUnion_range_ι_comp_ψ {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] {S : Set ↥X} (hS : IsClosed S) (Q : (p : { p : ↥X // IsClosed {p} ∧ p ∈ S }) → EtaleNbhdPair X ↑p) (V : (p : { p : ↥X // IsClosed {p} ∧ p ∈ S }) → (Q p).W.Opens) (hV : ∀ (p : { p : ↥X // IsClosed {p} ∧ p ∈ S }), (Q p).q ∈ V p) : S ⊆ ⋃ (p : { p : ↥X // IsClosed {p} ∧ p ∈ S }), Set.range ⇑(CategoryTheory.CategoryStruct.comp (V p).ι (Q p).ψ)

The images ψ_p(V p), over the closed points p of a closed set S, cover S: the closed points are dense in every closed subset of the Jacobson space X.

theorem AlgebraicGeometry.subset_iUnion_range_ι_comp_ψ' {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] {S : Set ↥X} (hS : IsClosed S) (Q : (p : { p : ↥X // IsClosed {p} ∧ p ∈ S }) → EtaleNbhdPair X ↑p) (V : (p : { p : ↥X // IsClosed {p} ∧ p ∈ S }) → (Q p).W.Opens) (hV : ∀ (p : { p : ↥X // IsClosed {p} ∧ p ∈ S }), (Q p).q ∈ V p) : S ⊆ ⋃ (p : { p : ↥X // IsClosed {p} ∧ p ∈ S }), Set.range ⇑(CategoryTheory.CategoryStruct.comp (V p).ι (Q p).ψ')

The images ψ'_p(V p) cover S as well.

theorem AlgebraicGeometry.exists_finset_subset_biUnion_range {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] [CompactSpace ↥X] {S : Set ↥X} (hS : IsClosed S) (Q : (p : { p : ↥X // IsClosed {p} ∧ p ∈ S }) → EtaleNbhdPair X ↑p) (V : (p : { p : ↥X // IsClosed {p} ∧ p ∈ S }) → (Q p).W.Opens) (hV : ∀ (p : { p : ↥X // IsClosed {p} ∧ p ∈ S }), (Q p).q ∈ V p) : ∃ (t : Finset { p : ↥X // IsClosed {p} ∧ p ∈ S }), S ⊆ ⋃ p ∈ t, Set.range ⇑(CategoryTheory.CategoryStruct.comp (V p).ι (Q p).ψ) ∧ S ⊆ ⋃ p ∈ t, Set.range ⇑(CategoryTheory.CategoryStruct.comp (V p).ι (Q p).ψ')

For X quasi-compact, finitely many closed points p_1, …, p_N of S have ⋃ ψ_{p_i}(V p_i) ⊇ S and ⋃ ψ'_{p_i}(V p_i) ⊇ S ("the images of finitely many of the U(p) cover X", [Kol07, 95]): cover S by the open sets ψ_p(V p) ∩ ψ'_p(V p) ∋ p and take a finite subcover of the compact closed set S.