Commit 2023-03-13 22:27 4b81ccf4

View on Github →

feat: port Topology.Semicontinuous (#2856)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Semicontinuous.lean

added theorem Continuous.comp_lowerSemicontinuous

added theorem Continuous.comp_lowerSemicontinuousOn

added theorem Continuous.comp_lowerSemicontinuousOn_antitone

added theorem Continuous.comp_lowerSemicontinuous_antitone

added theorem Continuous.comp_upperSemicontinuous

added theorem Continuous.comp_upperSemicontinuousOn

added theorem Continuous.comp_upperSemicontinuousOn_antitone

added theorem Continuous.comp_upperSemicontinuous_antitone

added theorem Continuous.lowerSemicontinuous

added theorem Continuous.upperSemicontinuous

added theorem ContinuousAt.comp_lowerSemicontinuousAt

added theorem ContinuousAt.comp_lowerSemicontinuousAt_antitone

added theorem ContinuousAt.comp_lowerSemicontinuousWithinAt

added theorem ContinuousAt.comp_lowerSemicontinuousWithinAt_antitone

added theorem ContinuousAt.comp_upperSemicontinuousAt

added theorem ContinuousAt.comp_upperSemicontinuousAt_antitone

added theorem ContinuousAt.comp_upperSemicontinuousWithinAt

added theorem ContinuousAt.comp_upperSemicontinuousWithinAt_antitone

added theorem ContinuousAt.lowerSemicontinuousAt

added theorem ContinuousAt.upperSemicontinuousAt

added theorem ContinuousOn.lowerSemicontinuousOn

added theorem ContinuousOn.upperSemicontinuousOn

added theorem ContinuousWithinAt.lowerSemicontinuousWithinAt

added theorem ContinuousWithinAt.upperSemicontinuousWithinAt

added theorem IsClosed.lowerSemicontinuousAt_indicator

added theorem IsClosed.lowerSemicontinuousOn_indicator

added theorem IsClosed.lowerSemicontinuousWithinAt_indicator

added theorem IsClosed.lowerSemicontinuous_indicator

added theorem IsClosed.upperSemicontinuousAt_indicator

added theorem IsClosed.upperSemicontinuousOn_indicator

added theorem IsClosed.upperSemicontinuousWithinAt_indicator

added theorem IsClosed.upperSemicontinuous_indicator

added theorem IsOpen.lowerSemicontinuousAt_indicator

added theorem IsOpen.lowerSemicontinuousOn_indicator

added theorem IsOpen.lowerSemicontinuousWithinAt_indicator

added theorem IsOpen.lowerSemicontinuous_indicator

added theorem IsOpen.upperSemicontinuousAt_indicator

added theorem IsOpen.upperSemicontinuousOn_indicator

added theorem IsOpen.upperSemicontinuousWithinAt_indicator

added theorem IsOpen.upperSemicontinuous_indicator

added theorem LowerSemicontinuous.add'

added theorem LowerSemicontinuous.add

added theorem LowerSemicontinuous.isClosed_preimage

added theorem LowerSemicontinuous.isOpen_preimage

added theorem LowerSemicontinuous.lowerSemicontinuousAt

added theorem LowerSemicontinuous.lowerSemicontinuousOn

added theorem LowerSemicontinuous.lowerSemicontinuousWithinAt

added def LowerSemicontinuous

added theorem LowerSemicontinuousAt.add'

added theorem LowerSemicontinuousAt.add

added theorem LowerSemicontinuousAt.lowerSemicontinuousWithinAt

added def LowerSemicontinuousAt

added theorem LowerSemicontinuousOn.add'

added theorem LowerSemicontinuousOn.add

added theorem LowerSemicontinuousOn.lowerSemicontinuousWithinAt

added theorem LowerSemicontinuousOn.mono

added def LowerSemicontinuousOn

added theorem LowerSemicontinuousWithinAt.add'

added theorem LowerSemicontinuousWithinAt.add

added theorem LowerSemicontinuousWithinAt.mono

added def LowerSemicontinuousWithinAt

added theorem UpperSemicontinuous.add'

added theorem UpperSemicontinuous.add

added theorem UpperSemicontinuous.isClosed_preimage

added theorem UpperSemicontinuous.isOpen_preimage

added theorem UpperSemicontinuous.upperSemicontinuousAt

added theorem UpperSemicontinuous.upperSemicontinuousOn

added theorem UpperSemicontinuous.upperSemicontinuousWithinAt

added def UpperSemicontinuous

added theorem UpperSemicontinuousAt.add'

added theorem UpperSemicontinuousAt.add

added theorem UpperSemicontinuousAt.upperSemicontinuousWithinAt

added def UpperSemicontinuousAt

added theorem UpperSemicontinuousOn.add'

added theorem UpperSemicontinuousOn.add

added theorem UpperSemicontinuousOn.mono

added theorem UpperSemicontinuousOn.upperSemicontinuousWithinAt

added def UpperSemicontinuousOn

added theorem UpperSemicontinuousWithinAt.add'

added theorem UpperSemicontinuousWithinAt.add

added theorem UpperSemicontinuousWithinAt.mono

added def UpperSemicontinuousWithinAt

added theorem continuousAt_iff_lower_upperSemicontinuousAt

added theorem continuousOn_iff_lower_upperSemicontinuousOn

added theorem continuousWithinAt_iff_lower_upperSemicontinuousWithinAt

added theorem continuous_iff_lower_upperSemicontinuous

added theorem lowerSemicontinuousAt_bsupr

added theorem lowerSemicontinuousAt_const

added theorem lowerSemicontinuousAt_csupr

added theorem lowerSemicontinuousAt_sum

added theorem lowerSemicontinuousAt_supᵢ

added theorem lowerSemicontinuousAt_tsum

added theorem lowerSemicontinuousOn_bsupr

added theorem lowerSemicontinuousOn_const

added theorem lowerSemicontinuousOn_csupr

added theorem lowerSemicontinuousOn_sum

added theorem lowerSemicontinuousOn_supᵢ

added theorem lowerSemicontinuousOn_tsum

added theorem lowerSemicontinuousOn_univ_iff

added theorem lowerSemicontinuousWithinAt_bsupr

added theorem lowerSemicontinuousWithinAt_const

added theorem lowerSemicontinuousWithinAt_csupr

added theorem lowerSemicontinuousWithinAt_sum

added theorem lowerSemicontinuousWithinAt_supᵢ

added theorem lowerSemicontinuousWithinAt_tsum

added theorem lowerSemicontinuousWithinAt_univ_iff

added theorem lowerSemicontinuous_bsupr

added theorem lowerSemicontinuous_const

added theorem lowerSemicontinuous_csupr

added theorem lowerSemicontinuous_iff_isClosed_preimage

added theorem lowerSemicontinuous_iff_isOpen_preimage

added theorem lowerSemicontinuous_sum

added theorem lowerSemicontinuous_supᵢ

added theorem lowerSemicontinuous_tsum

added theorem upperSemicontinuousAt_binfi

added theorem upperSemicontinuousAt_cinfi

added theorem upperSemicontinuousAt_const

added theorem upperSemicontinuousAt_infᵢ

added theorem upperSemicontinuousAt_sum

added theorem upperSemicontinuousOn_binfi

added theorem upperSemicontinuousOn_cinfi

added theorem upperSemicontinuousOn_const

added theorem upperSemicontinuousOn_infᵢ

added theorem upperSemicontinuousOn_sum

added theorem upperSemicontinuousOn_univ_iff

added theorem upperSemicontinuousWithinAt_binfi

added theorem upperSemicontinuousWithinAt_cinfi

added theorem upperSemicontinuousWithinAt_const

added theorem upperSemicontinuousWithinAt_infᵢ

added theorem upperSemicontinuousWithinAt_sum

added theorem upperSemicontinuousWithinAt_univ_iff

added theorem upperSemicontinuous_binfi

added theorem upperSemicontinuous_cinfi

added theorem upperSemicontinuous_const

added theorem upperSemicontinuous_iff_isClosed_preimage

added theorem upperSemicontinuous_iff_isOpen_preimage

added theorem upperSemicontinuous_infᵢ

added theorem upperSemicontinuous_sum