Locally Noetherian and Noetherian schemes

Let $X$ be a scheme. For an open subset $U \subseteq X$ write $\Gamma(X,U)=\mathcal O_X(U)$ for its ring of sections; when $U$ is an open affine subset, $U \cong \operatorname{Spec}\Gamma(X,U)$.

1. $X$ is locally Noetherian if every point $x \in X$ lies in some open affine $U$ with $\Gamma(X,U)$ a Noetherian ring, i.e. $X$ is covered by open affines $U \cong \operatorname{Spec} A$ with $A$ Noetherian.
2. $X$ is Noetherian if there are finitely many open affines $U_1,\dots,U_n$ with

These are the two notions every statement of this mission is phrased in. They are stated directly from the source's definition, not through Mathlib's AlgebraicGeometry.IsLocallyNoetherian / AlgebraicGeometry.IsNoetherian (which use "every affine open has Noetherian sections" as the definition); the equivalence of the two is part of the mission.

Formalization Note An open affine $U \cong \operatorname{Spec} A$ has $A \cong \Gamma(X,U)$, so "covered by spectra of Noetherian rings" is encoded as "covered by affine opens whose rings of sections are Noetherian". The empty scheme is Noetherian (empty cover).