Theorem lowerSemicontinuousWithinAt_iff_le_liminf

Modification history

2024-02-29 14:27
Mathlib/Topology/Semicontinuous.lean
feat: Equivalent characterizations of lower- and upper-semicontinuous functions (#7851) …
Added lowerSemicontinuousWithinAt_iff_le_liminfView on Github →