Commit 2024-02-29 14:27 45041bba

View on Github →

feat: Equivalent characterizations of lower- and upper-semicontinuous functions (#7851) We add lowerSemicontinuousAt_iff_le_liminf, lowerSemicontinuous_iff_IsClosed_epigraph and variants.

Estimated changes

Modified Mathlib/Topology/Semicontinuous.lean

added theorem lowerSemicontinuousAt_iff_le_liminf

added theorem lowerSemicontinuousOn_iff_le_liminf

added theorem lowerSemicontinuousWithinAt_iff_le_liminf

added theorem lowerSemicontinuous_iff_IsClosed_epigraph

added theorem lowerSemicontinuous_iff_le_liminf

added theorem upperSemicontinuousAt_iff_limsup_le

added theorem upperSemicontinuousOn_iff_limsup_le

added theorem upperSemicontinuousWithinAt_iff_limsup_le

added theorem upperSemicontinuous_iff_IsClosed_hypograph

added theorem upperSemicontinuous_iff_limsup_le