pointwise): The closure of a thickening (#13708)

Commit

3 years ago

feat(analysis/normed_space/pointwise): The closure of a thickening (#13708) Prove `closure (thickening δ s) = cthickening δ s` and golf "thickening a thickening" lemmas.

Author

YaelDillies

Parents

e6c6764d

mathlib bfa0ba5b - feat(analysis/normed_space/pointwise): The closure of a thickening (#13708)

mathlib
bfa0ba5b - feat(analysis/normed_space/pointwise): The closure of a thickening (#13708)