Mathlib v3 is deprecated. Go to Mathlib v4

Theorem upper_semicontinuous_iff_is_open_preimage

Modification history

2022-09-30 23:37

src/topology/semicontinuous.lean

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

Added upper_semicontinuous_iff_is_open_preimage View on Github →