Theorem LowerSemicontinuous.comp_continuous

Modification history

2025-12-17 18:54
Mathlib/Topology/Semicontinuity/Basic.lean
refactor: generalize semicontinuity (#32521) …
Deleted LowerSemicontinuous.comp_continuousView on Github →
2024-03-15 16:00
Mathlib/Topology/Semicontinuous.lean
feat: Semicontinuity of `f ∘ g` for `f` semicontinuous, `g` continuous (#10822) …
Added LowerSemicontinuous.comp_continuousView on Github →