Mathlib v3 is deprecated. Go to Mathlib v4

Theorem upper_semicontinuous.is_closed_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.is_closed_preimage View on Github →