mathlib

c1a28cb2 - feat(topology/semicontinuous): characterization by closed sets of semicontinuous maps to a linear order (#16442)