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

Prove `closure (thickening δ s) = cthickening δ s` and golf "thickening a thickening" lemmas.





leanprover-community/mathlib,leanprover-community/mathlib