Commit 2024-03-15 16:00 aae7c58b

View on Github →

feat: Semicontinuity of f ∘ g for f semicontinuous, g continuous (#10822) Only the other direction exists currently, it seems.

Estimated changes

Modified Mathlib/Topology/Semicontinuous.lean

added theorem LowerSemicontinuous.comp_continuous

added theorem LowerSemicontinuousAt.comp_continuousAt

added theorem LowerSemicontinuousAt.comp_continuousAt_of_eq

added theorem UpperSemicontinuous.comp_continuous

added theorem UpperSemicontinuousAt.comp_continuousAt

added theorem UpperSemicontinuousAt.comp_continuousAt_of_eq