Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-07-14 12:56
3b7e7bd6
View on Github →
feat(normed_space): controlled_sum_of_mem_closure (
#8310
) From LTE
Estimated changes
Modified
src/analysis/normed_space/basic.lean
added
theorem
controlled_sum_of_mem_closure
added
theorem
controlled_sum_of_mem_closure_range
Modified
src/order/filter/at_top_bot.lean
deleted
theorem
filter.strict_mono_tendsto_at_top
added
theorem
strict_mono.tendsto_at_top