Skip to content

[Merged by Bors] - feat: Sigma-algebra generated by a singleton#2513

Closed
YaelDillies wants to merge 7 commits intomasterfrom
generate_from_singleton
Closed

[Merged by Bors] - feat: Sigma-algebra generated by a singleton#2513
YaelDillies wants to merge 7 commits intomasterfrom
generate_from_singleton

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Feb 27, 2023

@YaelDillies YaelDillies added the mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged label Feb 27, 2023
@YaelDillies YaelDillies mentioned this pull request Feb 27, 2023
Closed
@eric-wieser eric-wieser added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 21, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Jul 17, 2023

I'll close this as it is empty and the mathlib3 PR was too-late. Just open a new PR with the content if you'd like.

@kim-em kim-em closed this Jul 17, 2023
@eric-wieser eric-wieser reopened this Sep 14, 2023
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Sep 14, 2023

The mathlib3 PR was merged, so lets re-open this one

@bors bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:24
@kim-em kim-em changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 12:18
@YaelDillies YaelDillies force-pushed the generate_from_singleton branch from 1b9c43c to 8576ebe Compare September 19, 2023 07:57
@YaelDillies YaelDillies added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-measure-probability Measure theory / Probability theory and removed awaiting-author A reviewer has asked the author a question or requested changes. forward-port-placeholder labels Sep 19, 2023
@YaelDillies YaelDillies mentioned this pull request Sep 19, 2023
Closed
1 task
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Sep 24, 2023
@RemyDegenne
Copy link
Copy Markdown
Contributor

RemyDegenne commented Sep 26, 2023

Thanks!
bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Sep 26, 2023
bors bot pushed a commit that referenced this pull request Sep 26, 2023
@YaelDillies
feat: Sigma-algebra generated by a singleton (#2513)
d84c8d2 
Match leanprover-community/mathlib3#18506
@bors
Copy link
Copy Markdown

bors bot commented Sep 26, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: Sigma-algebra generated by a singleton [Merged by Bors] - feat: Sigma-algebra generated by a singleton Sep 26, 2023
@bors bors bot closed this Sep 26, 2023
@bors bors bot deleted the generate_from_singleton branch September 26, 2023 13:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged ready-to-merge This PR has been sent to bors. t-measure-probability Measure theory / Probability theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@YaelDillies @kim-em @eric-wieser @RemyDegenne