Commit 2026-03-17 17:53 310419d6

View on Github →

feat: f is lowersemicontinuous iff -f is uppersemicontinuous (#36598) Proved that a function f is lowersemicontinuous iff -f is uppersemicontinuous. Also changed the hypothesis of upperSemicontinuousOn_iff_preimage_Iio from LinearOrder to Preorder. Used in the proof of conditional Jensen's inequality for concave functions.

Estimated changes

Modified Mathlib/Topology/Semicontinuity/Basic.lean

added theorem lowerSemiContinuous_inv_iff

added theorem lowerSemicontinuouAt_inv_iff

added theorem lowerSemicontinuousOn_inv_iff

added theorem lowerSemicontinuousWithinAt_inv_iff

added theorem upperSemiContinuous_inv_iff

added theorem upperSemicontinuousAt_inv_iff

modified theorem upperSemicontinuousOn_iff_preimage_Ici

modified theorem upperSemicontinuousOn_iff_preimage_Iio

added theorem upperSemicontinuousOn_inv_iff

added theorem upperSemicontinuousWithinAt_inv_iff