Skip to content

[Merged by Bors] - feat: product of filtered categories is filtered#18979

Closed
TwoFX wants to merge 1 commit intomasterfrom
fme-157
Closed

[Merged by Bors] - feat: product of filtered categories is filtered#18979
TwoFX wants to merge 1 commit intomasterfrom
fme-157

Conversation

@TwoFX
Copy link
Copy Markdown
Member

@TwoFX TwoFX commented Nov 13, 2024

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 13, 2024

PR summary 5b8a038a0d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ instance [IsCofiltered C] [IsCofiltered D] : IsCofiltered (C × D)
+ instance [IsCofilteredOrEmpty C] [IsCofilteredOrEmpty D] : IsCofilteredOrEmpty (C × D)
+ instance [IsFiltered C] [IsFiltered D] : IsFiltered (C × D)
+ instance [IsFilteredOrEmpty C] [IsFilteredOrEmpty D] : IsFilteredOrEmpty (C × D)
+ instance [∀ i, IsCofiltered (I i)] : IsCofiltered (∀ i, I i)
+ instance [∀ i, IsCofilteredOrEmpty (I i)] : IsCofilteredOrEmpty (∀ i, I i)
+ instance [∀ i, IsFiltered (I i)] : IsFiltered (∀ i, I i)
+ instance [∀ i, IsFilteredOrEmpty (I i)] : IsFilteredOrEmpty (∀ i, I i)

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

@github-actions github-actions bot added the t-category-theory Category theory label Nov 13, 2024
@TwoFX TwoFX mentioned this pull request Nov 13, 2024
Closed
5 tasks
@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Nov 13, 2024

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Nov 13, 2024
mathlib-bors bot pushed a commit that referenced this pull request Nov 13, 2024
@TwoFX
feat: product of filtered categories is filtered (#18979)
0014318 
Co-authored-by: Markus Himmel <markus@lean-fro.org>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 13, 2024

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Nov 13, 2024
@TwoFX
feat: product of filtered categories is filtered (#18979)
a968f11 
Co-authored-by: Markus Himmel <markus@lean-fro.org>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 13, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: product of filtered categories is filtered [Merged by Bors] - feat: product of filtered categories is filtered Nov 13, 2024
@mathlib-bors mathlib-bors bot closed this Nov 13, 2024
@mathlib-bors mathlib-bors bot deleted the fme-157 branch November 13, 2024 21:59
TobiasLeichtfried pushed a commit that referenced this pull request Nov 21, 2024
@TwoFX @TobiasLeichtfried
feat: product of filtered categories is filtered (#18979)
b2efc55 
Co-authored-by: Markus Himmel <markus@lean-fro.org>
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

ready-to-merge This PR has been sent to bors. t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@TwoFX @joelriou