strongly_measurable): use `expand_exists` for `exists_set_sigma_finite`
#15718

Open

chore(measure_theory/function/strongly_measurable): use `expand_exists` for `exists_set_sigma_finite` #15718

RemyDegenne wants to merge 7 commits into master from RD_expand_exists

exists_set_sigma_finite

d0e3a038

restore protected attribute

c251f787

restore instance attribute

7ea9c7c0

add docstring

36e194bd

shorten names

69a8b594

docstring

98e433e8

RemyDegenne added awaiting-review

remove variables, put them in the lemma

7b7bf239

hrmacbeth added t-analysis

ghost added blocked-by-other-PR

RemyDegenne removed awaiting-review

RemyDegenne added awaiting-author

RemyDegenne removed t-analysis

RemyDegenne added t-measure-probability

kim-em added too-late

eric-wieser requested a review 2 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

awaiting-author blocked-by-other-PR t-measure-probability too-late

Milestone

No milestone