Lifting closed points from the image of a Jacobson space

For a continuous map from a Jacobson space, every closed point in its image has a closed lift. Indeed, its nonempty closed fiber contains a closed point by nonempty_inter_closedPoints. This is the topological input for closed-point lifting along morphisms locally of finite type into Jacobson schemes.

theorem Continuous.exists_isClosed_singleton_of_mem_range {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [JacobsonSpace X] {f : X → Y} (hf : Continuous f) {y : Y} (hy : IsClosed {y}) (hyf : y ∈ Set.range f) : ∃ (x : X), IsClosed {x} ∧ f x = y

Every closed point in the image of a continuous map from a Jacobson space has a closed lift.