Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-03-20 23:19
e20c7304
View on Github →
feat(topology/continuous_map): formulas for sup and inf in terms of abs (
#6720
)
Estimated changes
Modified
src/algebra/ordered_group.lean
added
theorem
sub_le_sub_flip
Modified
src/topology/algebra/continuous_functions.lean
added
theorem
continuous_map.inf_eq
added
theorem
continuous_map.sup_eq
added
theorem
div_coe
added
theorem
max_eq_half_add_add_abs_sub
added
theorem
min_eq_half_add_sub_abs_sub
Modified
src/topology/continuous_map.lean
added
def
continuous_map.abs
added
theorem
continuous_map.abs_apply