Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-01-05 22:31
771d1449
View on Github →
feat(analysis/normed_space/lp_space): completeness of the lp space on
Π i, E i
(
#11094
)
Estimated changes
Modified
src/analysis/normed/group/basic.lean
added
theorem
normed_group.uniformity_basis_dist
Modified
src/analysis/normed/group/pointwise.lean
added
theorem
metric.bounded.exists_pos_norm_le
Modified
src/analysis/normed_space/lp_space.lean
added
theorem
lp.mem_ℓp_of_tendsto
added
theorem
lp.norm_apply_le_norm
added
theorem
lp.norm_apply_le_of_tendsto
added
theorem
lp.norm_le_of_forall_le'
added
theorem
lp.norm_le_of_forall_le
added
theorem
lp.norm_le_of_forall_sum_le
added
theorem
lp.norm_le_of_tendsto
added
theorem
lp.norm_le_of_tsum_le
added
theorem
lp.sum_rpow_le_norm_rpow
added
theorem
lp.sum_rpow_le_of_tendsto
added
theorem
lp.tendsto_lp_of_tendsto_pi
added
theorem
lp.uniform_continuous_coe
added
theorem
mem_ℓp_gen'
modified
theorem
mem_ℓp_gen
Modified
src/order/filter/at_top_bot.lean
added
theorem
filter.eventually_at_bot_curry
added
theorem
filter.eventually_at_top_curry
Modified
src/topology/algebra/infinite_sum.lean
added
theorem
finite_of_summable_const
Modified
src/topology/uniform_space/cauchy.lean
added
theorem
cauchy_seq.eventually_eventually