∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [inst : AlgebraicGeometry.LocallyOfFiniteType f] {x : ↥X},
  x ∈ AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus f ↔ AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt f x