[Merged by Bors] - feat(MeasureTheory/Measure/Tight): portmanteau condition for compact sets#39543

Closed

jvanwinden wants to merge 20 commits into

leanprover-community:masterfrom

jvanwinden:portmanteau_compact

Commits on May 18, 2026

add lemma
Joris van Winden
committed

Commits on May 28, 2026

add docstring and remove T2space assumption
Joris van Winden
committed

Commits on May 29, 2026

implement reviewer suggestions
Joris van Winden
committed
move declerations to different files
Joris van Winden
committed
cleanup prokhorov file
Joris van Winden
committed
put the new result at a better location
Joris van Winden
committed

Commits on May 30, 2026

minimize imports in Tight
Joris van Winden
committed
minimize imports in Portmanteau
Joris van Winden
committed
minimize imports in Prokhorov
Joris van Winden
committed
remove min_imports command
Joris van Winden
committed
add back imports in Tight
Joris van Winden
committed

Commits on Jun 1, 2026

apply suggestions in Tight
Joris van Winden
committed
apply suggestions in portmanteau
Joris van Winden
committed
apply suggestions in Prokhorov
Joris van Winden
committed
apply more suggestions
Joris van Winden
committed
Merge branch 'master' into portmanteau_compact
jvanwinden
authored
fix imports in Tight
Joris van Winden
committed
fix downstream import issue
Joris van Winden
committed
fix more downstream imports
Joris van Winden
committed

Commits on Jun 2, 2026

fix imports
Joris van Winden
committed