[Merged by Bors] - feat(Algebra/Group/Pointwise/Set/Basic): sInter and sUnion forms of pointwise operations by mans0954 · Pull Request #17253 · leanprover-community/mathlib4

mans0954 · 2024-09-29T13:27:04Z

Provides sInter and sUnion versions of pointwise algebraic operations on sets.

Needed in #17029

github-actions · 2024-09-29T13:27:51Z

PR summary 2e23193276

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ div_sInter_subset
+ div_sUnion
+ image2_sInter_left_subset
+ image2_sInter_right_subset
+ image2_sInter_subset_left
+ image2_sInter_subset_right
+ image2_sUnion_left
+ image2_sUnion_right
+ mul_sInter_subset
+ mul_sUnion
+ sInter_div_subset
+ sInter_inv
+ sInter_mul_subset
+ sInter_smul_subset
+ sInter_vsub_subset
+ sUnion_div
+ sUnion_inv
+ sUnion_mul
+ sUnion_smul
+ sUnion_vsub
+ smul_sInter_subset
+ smul_sUnion
+ smul_set_sInter_subset
+ smul_set_sUnion
+ vsub_sInter_subset
+ vsub_sUnion

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.

Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

Mathlib/Data/Set/Lattice.lean

Co-authored-by: Yaël Dillies <[email protected]>

Co-authored-by: Bhavik Mehta <[email protected]>

Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

Mathlib/Data/Set/Lattice.lean

Co-authored-by: Yaël Dillies <[email protected]>

…y/mathlib4 into mans0954/smul-lemmas

Co-authored-by: Yaël Dillies <[email protected]>

YaelDillies

Thanks!

maintainer merge

github-actions · 2024-09-30T18:54:22Z

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

b-mehta · 2024-09-30T20:40:24Z

Thanks!

bors merge

…ointwise operations (#17253) Provides `sInter` and `sUnion` versions of pointwise algebraic operations on sets. Needed in #17029 Co-authored-by: Christopher Hoskin <[email protected]>

mathlib-bors · 2024-09-30T21:32:19Z

Pull request successfully merged into master.

Build succeeded:

…ointwise operations (#17253) Provides `sInter` and `sUnion` versions of pointwise algebraic operations on sets. Needed in #17029 Co-authored-by: Christopher Hoskin <[email protected]>

Extract results from #17029

7a3b456

mans0954 requested a review from YaelDillies September 29, 2024 13:27

mans0954 added the t-algebra Algebra (groups, rings, fields, etc) label Sep 29, 2024

mans0954 mentioned this pull request Sep 29, 2024

[Merged by Bors] - feat(Analysis/LocallyConvex/AbsConvex): Define the Absolutely Convex Hull #17029

Closed

1 task

Add sInter_smul_subset

2b1ff1a

mans0954 added WIP Work in progress awaiting-author A reviewer has asked the author a question or requested changes. labels Sep 29, 2024

mans0954 added 5 commits September 29, 2024 15:16

mul_sInter_subset and sInter_mul_subset

e6e5840

sInter_inv

c9ecabc

Add sInter_div_subset and div_sInter_subset

ce641f7

Put smul_iInter_subset and sInter_smul_subset in the right place

f8d26be

Add sInter_vsub_subset and vsub_sInter_subset

e72812a

mans0954 changed the title ~~feature(Algebra/Group/Pointwise/Set/Basic): Some smul lemmas~~ feature(Algebra/Group/Pointwise/Set/Basic): sInter forms of pointwise operations Sep 29, 2024

Also add the sUnion results

ec8f184

mans0954 changed the title ~~feature(Algebra/Group/Pointwise/Set/Basic): sInter forms of pointwise operations~~ feature(Algebra/Group/Pointwise/Set/Basic): sInter and sUnion forms of pointwise operations Sep 29, 2024

mans0954 removed WIP Work in progress awaiting-author A reviewer has asked the author a question or requested changes. labels Sep 29, 2024

mans0954 assigned YaelDillies Sep 29, 2024

YaelDillies reviewed Sep 30, 2024

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 30, 2024

b-mehta reviewed Sep 30, 2024

View reviewed changes

Mathlib/Data/Set/Lattice.lean Outdated Show resolved Hide resolved

Mathlib/Data/Set/Lattice.lean Outdated Show resolved Hide resolved

mans0954 and others added 8 commits September 30, 2024 17:57

Update Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

ca1cace

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

56a2896

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

b4285a5

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

942c1ea

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

7bcc847

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

a82bc0f

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

05e36f1

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

c1fd4fd

Co-authored-by: Yaël Dillies <[email protected]>

mans0954 and others added 7 commits September 30, 2024 17:58

Update Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

78a1167

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

548be28

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

64c0043

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

d9c3a6b

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Data/Set/Lattice.lean

3551a1d

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Data/Set/Lattice.lean

421abd5

Co-authored-by: Bhavik Mehta <[email protected]>

Update Mathlib/Data/Set/Lattice.lean

b0021f7

Co-authored-by: Bhavik Mehta <[email protected]>

mans0954 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 30, 2024

YaelDillies changed the title ~~feature(Algebra/Group/Pointwise/Set/Basic): sInter and sUnion forms of pointwise operations~~ feat(Algebra/Group/Pointwise/Set/Basic): sInter and sUnion forms of pointwise operations Sep 30, 2024

Merge branch 'master' into mans0954/smul-lemmas

4decff1

YaelDillies reviewed Sep 30, 2024

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 30, 2024

mans0954 and others added 6 commits September 30, 2024 18:16

Update Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

1ebb5a7

Co-authored-by: Yaël Dillies <[email protected]>

Golf

32c47d5

Merge branch 'mans0954/smul-lemmas' of github.com:leanprover-communit…

86e0592

…y/mathlib4 into mans0954/smul-lemmas

Golf

9956c59

Update Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

542c165

Co-authored-by: Yaël Dillies <[email protected]>

_ _ -> ..

2e23193

mans0954 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 30, 2024

YaelDillies approved these changes Sep 30, 2024

View reviewed changes

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 30, 2024

github-actions bot added the ready-to-merge This PR has been sent to bors. label Sep 30, 2024

mathlib-bors bot changed the title ~~feat(Algebra/Group/Pointwise/Set/Basic): sInter and sUnion forms of pointwise operations~~ [Merged by Bors] - feat(Algebra/Group/Pointwise/Set/Basic): sInter and sUnion forms of pointwise operations Sep 30, 2024

mathlib-bors bot closed this Sep 30, 2024

mathlib-bors bot deleted the mans0954/smul-lemmas branch September 30, 2024 21:32

Conversation

mans0954 commented Sep 29, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Sep 29, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 2e23193276

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Sep 30, 2024

Uh oh!

b-mehta commented Sep 30, 2024

Uh oh!

mathlib-bors bot commented Sep 30, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

mans0954 commented Sep 29, 2024 •

edited

Loading

github-actions bot commented Sep 29, 2024 •

edited

Loading