mathlib3
7b7bf239 - remove variables, put them in the lemma

Commit

3 years ago

remove variables, put them in the lemma

References

RD_expand_exists

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

Author

RemyDegenne

RemyDegenne

Parents

Loading