Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-30 23:37 c1a28cb2

View on Github →

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

Estimated changes

Modified src/topology/semicontinuous.lean

added theorem lower_semicontinuous.is_closed_preimage

added theorem lower_semicontinuous_iff_is_closed_preimage

deleted theorem lower_semicontinuous_iff_is_open

added theorem lower_semicontinuous_iff_is_open_preimage

added theorem upper_semicontinuous.is_closed_preimage

added theorem upper_semicontinuous_iff_is_closed_preimage

deleted theorem upper_semicontinuous_iff_is_open

added theorem upper_semicontinuous_iff_is_open_preimage