Theorem open_iff_inter_of_supr_eq_top

feat(algebraic_geometry/morphisms/universally_closed): Define universally closed morphism between schemes (#17117)

feat(topology/local_at_target): Properties of continuous maps that are local at the target. (#15452)