mathlib3

d9767b54 - feat(measure_theory/measure/portmanteau): Add lemmas in preparation of implication from Borel condition. (#17962)

feat(measure_theory/measure/portmanteau): Add lemmas in preparation of implication from Borel condition. (#17962) Add the essential lemmas about the existence of thickenings with null frontier that are needed to prove the portmanteau implication from Borel set condition to closed set condition.