Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-27 00:46 20291d00

View on Github →

feat(topology/semicontinuous): basics on lower and upper semicontinuous functions (#7693) We mimick the interface for continuity, by introducing predicates lower_semicontinuous_within_at, lower_semicontinuous_at, lower_semicontinuous_on and lower_semicontinuous (and similarly for upper semicontinuity).

Estimated changes

Modified src/algebra/ordered_monoid.lean

Modified src/topology/algebra/ordered/basic.lean

Modified src/topology/constructions.lean

added theorem mem_nhds_prod_iff'

Created src/topology/semicontinuous.lean

added theorem continuous.lower_semicontinuous

added theorem continuous.upper_semicontinuous

added theorem continuous_at.lower_semicontinuous_at

added theorem continuous_at.upper_semicontinuous_at

added theorem continuous_at_iff_lower_upper_semicontinuous_at

added theorem continuous_iff_lower_upper_semicontinuous

added theorem continuous_on.lower_semicontinuous_on

added theorem continuous_on.upper_semicontinuous_on

added theorem continuous_on_iff_lower_upper_semicontinuous_on

added theorem continuous_within_at.lower_semicontinuous_within_at

added theorem continuous_within_at.upper_semicontinuous_within_at

added theorem continuous_within_at_iff_lower_upper_semicontinuous_within_at

added theorem is_closed.lower_semicontinuous_at_indicator

added theorem is_closed.lower_semicontinuous_indicator

added theorem is_closed.lower_semicontinuous_on_indicator

added theorem is_closed.lower_semicontinuous_within_at_indicator

added theorem is_closed.upper_semicontinuous_at_indicator

added theorem is_closed.upper_semicontinuous_indicator

added theorem is_closed.upper_semicontinuous_on_indicator

added theorem is_closed.upper_semicontinuous_within_at_indicator

added theorem is_open.lower_semicontinuous_at_indicator

added theorem is_open.lower_semicontinuous_indicator

added theorem is_open.lower_semicontinuous_on_indicator

added theorem is_open.lower_semicontinuous_within_at_indicator

added theorem is_open.upper_semicontinuous_at_indicator

added theorem is_open.upper_semicontinuous_indicator

added theorem is_open.upper_semicontinuous_on_indicator

added theorem is_open.upper_semicontinuous_within_at_indicator

added theorem lower_semicontinuous.add'

added theorem lower_semicontinuous.add

added theorem lower_semicontinuous.is_open_preimage

added theorem lower_semicontinuous.lower_semicontinuous_at

added theorem lower_semicontinuous.lower_semicontinuous_on

added theorem lower_semicontinuous.lower_semicontinuous_within_at

added def lower_semicontinuous

added theorem lower_semicontinuous_at.add'

added theorem lower_semicontinuous_at.add

added theorem lower_semicontinuous_at.lower_semicontinuous_within_at

added def lower_semicontinuous_at

added theorem lower_semicontinuous_at_bsupr

added theorem lower_semicontinuous_at_const

added theorem lower_semicontinuous_at_sum

added theorem lower_semicontinuous_at_supr

added theorem lower_semicontinuous_at_tsum

added theorem lower_semicontinuous_bsupr

added theorem lower_semicontinuous_const

added theorem lower_semicontinuous_iff_is_open

added theorem lower_semicontinuous_on.add'

added theorem lower_semicontinuous_on.add

added theorem lower_semicontinuous_on.lower_semicontinuous_within_at

added theorem lower_semicontinuous_on.mono

added def lower_semicontinuous_on

added theorem lower_semicontinuous_on_bsupr

added theorem lower_semicontinuous_on_const

added theorem lower_semicontinuous_on_sum

added theorem lower_semicontinuous_on_supr

added theorem lower_semicontinuous_on_tsum

added theorem lower_semicontinuous_on_univ_iff

added theorem lower_semicontinuous_sum

added theorem lower_semicontinuous_supr

added theorem lower_semicontinuous_tsum

added theorem lower_semicontinuous_within_at.add'

added theorem lower_semicontinuous_within_at.add

added theorem lower_semicontinuous_within_at.mono

added def lower_semicontinuous_within_at

added theorem lower_semicontinuous_within_at_bsupr

added theorem lower_semicontinuous_within_at_const

added theorem lower_semicontinuous_within_at_sum

added theorem lower_semicontinuous_within_at_supr

added theorem lower_semicontinuous_within_at_tsum

added theorem lower_semicontinuous_within_at_univ_iff

added theorem upper_semicontinuous.add'

added theorem upper_semicontinuous.add

added theorem upper_semicontinuous.is_open_preimage

added theorem upper_semicontinuous.upper_semicontinuous_at

added theorem upper_semicontinuous.upper_semicontinuous_on

added theorem upper_semicontinuous.upper_semicontinuous_within_at

added def upper_semicontinuous

added theorem upper_semicontinuous_at.add'

added theorem upper_semicontinuous_at.add

added theorem upper_semicontinuous_at.upper_semicontinuous_within_at

added def upper_semicontinuous_at

added theorem upper_semicontinuous_at_binfi

added theorem upper_semicontinuous_at_const

added theorem upper_semicontinuous_at_infi

added theorem upper_semicontinuous_at_sum

added theorem upper_semicontinuous_binfi

added theorem upper_semicontinuous_const

added theorem upper_semicontinuous_iff_is_open

added theorem upper_semicontinuous_infi

added theorem upper_semicontinuous_on.add'

added theorem upper_semicontinuous_on.add

added theorem upper_semicontinuous_on.mono

added theorem upper_semicontinuous_on.upper_semicontinuous_within_at

added def upper_semicontinuous_on

added theorem upper_semicontinuous_on_binfi

added theorem upper_semicontinuous_on_const

added theorem upper_semicontinuous_on_infi

added theorem upper_semicontinuous_on_sum

added theorem upper_semicontinuous_on_univ_iff

added theorem upper_semicontinuous_sum

added theorem upper_semicontinuous_within_at.add'

added theorem upper_semicontinuous_within_at.add

added theorem upper_semicontinuous_within_at.mono

added def upper_semicontinuous_within_at

added theorem upper_semicontinuous_within_at_binfi

added theorem upper_semicontinuous_within_at_const

added theorem upper_semicontinuous_within_at_infi

added theorem upper_semicontinuous_within_at_sum

added theorem upper_semicontinuous_within_at_univ_iff