Theorem upperSemicontinuousOn_iff_preimage_Ici

Modification history

2026-03-17 17:53
Mathlib/Topology/Semicontinuity/Basic.lean
feat: f is lowersemicontinuous iff -f is uppersemicontinuous (#36598) …
Modified upperSemicontinuousOn_iff_preimage_IciView on Github →
2025-11-01 17:18
Mathlib/Topology/Semicontinuous.lean
feat(Topology/Semicontinuous): lower bounds on compact sets (#29976) …
Added upperSemicontinuousOn_iff_preimage_IciView on Github →