Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(data/{list,multiset,finset}/*): attach and filter lemmas #18087

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - feat(data/{list,multiset,finset}/*): attach and filter lemmas #18087

wants to merge 13 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Jan 7, 2023 •
edited
Loading

Left commutativity and cardinality of list.filter/multiset.filter/finset.filter. Interaction of count/countp and attach.

Match leanprover-community/mathlib4#1470

Open in Gitpod

@YaelDillies YaelDillies mentioned this pull request Jan 7, 2023
Closed
4 tasks
@YaelDillies YaelDillies added the awaiting-review The author would like community review of the PR label Jan 7, 2023
@YaelDillies YaelDillies mentioned this pull request Jan 10, 2023
Closed
@eric-wieser eric-wieser 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 Feb 27, 2023
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 22, 2023
@kim-em kim-em added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Mar 28, 2023
@eric-wieser eric-wieser added the not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 label Jul 15, 2023
@kim-em
Copy link
Collaborator

kim-em commented Jul 30, 2023

LGTM. @eric-wieser? Further comments?

jcommelin
jcommelin approved these changes Oct 30, 2023
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Oct 30, 2023
bors bot pushed a commit that referenced this pull request Oct 30, 2023
@YaelDillies
feat(data/{list,multiset,finset}/*): attach and filter lemmas (#1…
65a1391 
…8087)

Left commutativity and cardinality of `list.filter`/`multiset.filter`/`finset.filter`. Interaction of `count`/`countp` and `attach`.
@bors
Copy link

bors bot commented Oct 30, 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(data/{list,multiset,finset}/*): attach and filter lemmas [Merged by Bors] - feat(data/{list,multiset,finset}/*): attach and filter lemmas Oct 30, 2023
@bors bors bot closed this Oct 30, 2023
@bors bors bot deleted the count_attach branch October 30, 2023 18:28
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 8, 2023
@YaelDillies
feat: attach and filter lemmas (#1470)
d36f6a1 
Match leanprover-community/mathlib3#18087
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 8, 2023
@YaelDillies
feat: attach and filter lemmas (#1470)
ffda3f2 
Match leanprover-community/mathlib3#18087
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 8, 2023
@YaelDillies
feat: attach and filter lemmas (#1470)
929a39d 
Match leanprover-community/mathlib3#18087
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 8, 2023
@YaelDillies
feat: attach and filter lemmas (#1470)
92d78f8 
Match leanprover-community/mathlib3#18087
grunweg pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 15, 2023
@YaelDillies @grunweg
feat: attach and filter lemmas (#1470)
4e2de98 
Match leanprover-community/mathlib3#18087
chenjulang added a commit to chenjulang/mathlib that referenced this pull request May 11, 2024
@chenjulang
Merge commit '65a1391a0106c9204fe45bc73a039f056558cb83'
08049e0 
* commit '65a1391a0106c9204fe45bc73a039f056558cb83': (12443 commits)
  feat(data/{list,multiset,finset}/*): `attach` and `filter` lemmas (leanprover-community#18087)
  feat(combinatorics/simple_graph): More clique lemmas (leanprover-community#19203)
  feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable (leanprover-community#16976)
  move old README.md to OLD_README.md
  doc: Add a warning mentioning Lean 4 to the readme (leanprover-community#19243)
  feat(topology/metric_space): diameter of pointwise zero and addition (leanprover-community#19028)
  feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods (leanprover-community#18629)
  feat(probability/independence): Independence of singletons (leanprover-community#18506)
  feat(combinatorics/set_family/ahlswede_zhang): Ahlswede-Zhang identity, part I (leanprover-community#18612)
  feat(data/finset/lattice): `sup'`/`inf'` lemmas (leanprover-community#18989)
  chore(order/liminf_limsup): Generalise and move lemmas (leanprover-community#18628)
  feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for abelian categories (leanprover-community#17926)
  feat(data/sum/interval): The lexicographic sum of two locally finite orders is locally finite (leanprover-community#11352)
  feat(analysis/convex/proj_Icc): Extending convex functions (leanprover-community#18797)
  feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for pseudoabelian categories (leanprover-community#17925)
  feat(measure_theory/measure/haar_quotient): the Unfolding Trick (leanprover-community#18863)
  feat(linear_algebra/orientation): add `orientation.reindex` (leanprover-community#19236)
  feat(combinatorics/quiver/covering): Definition of coverings and unique lifting of paths (leanprover-community#17828)
  feat(set_theory/game/pgame): small sets of pre-games / games / surreals are bounded (leanprover-community#15260)
  feat(tactic/positivity): Extension for `ite` (leanprover-community#17650)
  ...

# Conflicts:
#	README.md
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@YaelDillies @kim-em @eric-wieser @jcommelin @leanprover-community-bot-assistant