Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-05-31 14:35
4555798c
View on Github →
feat(topology/semicontinuous): semicontinuity of compositions (
#7763
)
Estimated changes
Modified
src/topology/semicontinuous.lean
added
theorem
continuous.comp_lower_semicontinuous
added
theorem
continuous.comp_lower_semicontinuous_antimono
added
theorem
continuous.comp_lower_semicontinuous_on
added
theorem
continuous.comp_lower_semicontinuous_on_antimono
added
theorem
continuous.comp_upper_semicontinuous
added
theorem
continuous.comp_upper_semicontinuous_antimono
added
theorem
continuous.comp_upper_semicontinuous_on
added
theorem
continuous.comp_upper_semicontinuous_on_antimono
added
theorem
continuous_at.comp_lower_semicontinuous_at
added
theorem
continuous_at.comp_lower_semicontinuous_at_antimono
added
theorem
continuous_at.comp_lower_semicontinuous_within_at
added
theorem
continuous_at.comp_lower_semicontinuous_within_at_antimono
added
theorem
continuous_at.comp_upper_semicontinuous_at
added
theorem
continuous_at.comp_upper_semicontinuous_at_antimono
added
theorem
continuous_at.comp_upper_semicontinuous_within_at
added
theorem
continuous_at.comp_upper_semicontinuous_within_at_antimono