theorem
noetherian_open_cover_finite
(X : Type u_1)
[TopologicalSpace X]
[TopologicalSpace.NoetherianSpace X]
(U : Set (Set X))
(hU : ∀ u ∈ U, IsOpen u)
(hcover : ⋃₀ U = Set.univ)
:
Every open cover of a Noetherian topological space admits a finite subcover. This underlies the fact that a variety has a finite open affine cover.