Skip to content
This repository has been 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
wants to merge 7 commits into
base: master
Choose a base branch
from
Open

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

wants to merge 7 commits into from

Conversation

RemyDegenne
Copy link
Collaborator

@RemyDegenne RemyDegenne commented Jul 27, 2022 •
edited
Loading

@RemyDegenne RemyDegenne added the awaiting-review The author would like community review of the PR label Jul 27, 2022
@hrmacbeth hrmacbeth added the t-analysis Analysis (normed *, calculus) label Jul 28, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@mathlib-dependent-issues-bot mathlib-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jul 28, 2022
@RemyDegenne RemyDegenne added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jul 29, 2022
@RemyDegenne RemyDegenne added t-measure-probability Measure theory / Probability theory and removed t-analysis Analysis (normed *, calculus) labels Sep 14, 2022
@kim-em kim-em added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023
@eric-wieser eric-wieser requested a review from a team as a code owner October 16, 2023 15:12
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-author A reviewer has asked the author a question or requested changes blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. t-measure-probability Measure theory / Probability theory too-late This PR was ready too late for inclusion in mathlib3
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@RemyDegenne @mathlib-dependent-issues-bot @kim-em @hrmacbeth