This repository was archived by the owner on Jul 24, 2024. It is now read-only.
chore(measure_theory/function/strongly_measurable): use expand_exists for exists_set_sigma_finite#15718
Open
RemyDegenne wants to merge 7 commits intomasterfrom RD_expand_exists
Commits
Commits on Jul 27, 2022
- committed
- committed
- committed
- committed
- committed
- committed
- committed
