[Merged by Bors] - feat: atoms of a countably generated measurable space

[mathlib-splicebot]

This PR adds a definition for the atoms in a countably generated measurable space, expressed with natGeneratingSequence.

We also show that the atoms are measurable sets.

---

This PR was automatically created from PR #39739 by @RemyDegenne via a review comment by @RemyDegenne.

[github-actions]

PR summary 160a411a68

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ countablyGeneratedAtom
+ disjoint_countablyGeneratedAtom
+ exists_eq_iUnion_countablyGeneratedAtom
+ iUnion_countablyGeneratedAtom
+ measurableAtom_eq_countablyGeneratedAtom_natGeneratingSequence
+ measurableSet_countablyGeneratedAtom
+ measurableSet_measurableAtom
+ mem_countablyGeneratedAtom_natGeneratingSequence

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 160a411a68
Reference commit 4533762966

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[gaetanserre]

Thanks! It looks good to me. I'm just wondering if there is a particular utility to define countablyGeneratedAtom with a general countable predicate instead of with a point x and (x ∈ natGeneratingSequence α ·) but I might miss something here.

[RemyDegenne]

The reason for defining it for a generic p : ℕ → Prop instead of only the one for a given point is that it's the way I found to actually have a working proof.

The end goal is to describe the atom of a given x. And that description follows from CountablyGenerated so the proof is most likely an induction using generateFrom_induction. I did not manage to make that work to prove that a given set is the atom of x directly. But I managed to use it to describe all sets as union of atoms in exists_eq_iUnion_countablyGeneratedAtom, and then deduce that the atom of x is one of those.

[gaetanserre]

Thanks for the explanation!

[EtienneC30]

Thanks!
maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by EtienneC30.

[sgouezel]

bors d+

[mathlib-bors]

✌️ mathlib-splicebot[bot] can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[bryangingechen]

We probably don't want to delegate to the bot.
bors d=@RemyDegenne

[mathlib-bors]

✌️ RemyDegenne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[RemyDegenne]

How do I push changes to this PR? I used gh pr checkout to get the branch, applied the changes suggested in reviews, and then tried to push, but it gets rejected. How are we supposed to work with those splicebot branches?

[EtienneC30]

I have no idea 😅 I just commit directly from the website.

[RemyDegenne]

bors r+

[mathlib-bors]

Canceled.

Address comments or fix if necessary, and then someone with permission can run bors r+.

[RemyDegenne]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job
• ci (staging) / Build
• ci (staging) / Lint style