[Merged by Bors] - feat(Data/Set/Intervals/Disjoint): i[Inter|Union]_Ii[c|o]... #10298

mo271 · 2024-02-06T13:27:12Z

mo271 · 2024-02-06T13:29:54Z

This prepares removing some lemmas from Probability/Kernel/CondCdf. Zulip discussion

urkud · 2024-02-11T04:09:47Z

Mathlib/Data/Set/Intervals/Disjoint.lean

@@ -253,4 +255,26 @@ theorem iUnion_Iic_eq_Iic_iSup {R : Type*} [CompleteLinearOrder R] {f : ι → R
  @iUnion_Ici_eq_Ici_iInf ι (OrderDual R) _ f has_greatest_elem
 #align Union_Iic_eq_Iic_supr iUnion_Iic_eq_Iic_iSup

+theorem iUnion_Iio_of_not_bddAbove_range (hf : ¬ BddAbove (range f)) :


Please add order-dual versions (probably using the OrderDual trick).

I thought the version below, now renamed iUnion_Iio_eq_univ_iff and iInter_Iio_eq_empty_iff are duals of each other. Do you mean some other sort of dual statement? If yes, which one?

ping @urkud

Mathlib/Data/Set/Intervals/Disjoint.lean

urkud · 2024-02-11T04:11:37Z

Mathlib/Data/Set/Intervals/Disjoint.lean

@@ -253,4 +255,26 @@ theorem iUnion_Iic_eq_Iic_iSup {R : Type*} [CompleteLinearOrder R] {f : ι → R
  @iUnion_Ici_eq_Ici_iInf ι (OrderDual R) _ f has_greatest_elem
 #align Union_Iic_eq_Iic_supr iUnion_Iic_eq_Iic_iSup

+theorem iUnion_Iio_of_not_bddAbove_range (hf : ¬ BddAbove (range f)) :
+    ⋃ i, Iio (f i) = univ := by
+  simpa [not_bddAbove_iff, Set.eq_univ_iff_forall] using hf


simpa says that it can be an iff lemma.

Made it an iff lemma.
Is the name good like this?

RemyDegenne

I just have comments about the names, to make them match the other lemmas you introduce. Apart from that, LGTM.
bors d+

Mathlib/Data/Set/Intervals/Disjoint.lean

mathlib-bors · 2024-03-26T11:54:39Z

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

mo271 · 2024-03-26T12:04:11Z

bors r+

Co-authored-by: Moritz Firsching <firsching@google.com>

mathlib-bors · 2024-03-26T12:38:23Z

Build failed (retrying...):

Build

mo271 · 2024-03-26T12:45:26Z

will fix the build...

Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

mathlib-bors · 2024-03-26T13:05:01Z

Canceled.

mo271 · 2024-03-26T13:05:32Z

fixed the name and rebased

mo271 · 2024-03-26T14:53:00Z

bors r+

Co-authored-by: Moritz Firsching <firsching@google.com>

mathlib-bors · 2024-03-26T16:32:54Z

Pull request successfully merged into master.

Build succeeded:

- [x] depends on: #10298 Co-authored-by: Moritz Firsching <firsching@google.com>

Co-authored-by: Moritz Firsching <firsching@google.com>

- [x] depends on: #10298 Co-authored-by: Moritz Firsching <firsching@google.com>

Co-authored-by: Moritz Firsching <firsching@google.com>

- [x] depends on: #10298 Co-authored-by: Moritz Firsching <firsching@google.com>

Co-authored-by: Moritz Firsching <firsching@google.com>

- [x] depends on: #10298 Co-authored-by: Moritz Firsching <firsching@google.com>

Co-authored-by: Moritz Firsching <firsching@google.com>

- [x] depends on: #10298 Co-authored-by: Moritz Firsching <firsching@google.com>

mo271 added awaiting-review The author would like community review of the PR awaiting-CI labels Feb 6, 2024

github-actions bot removed the awaiting-CI label Feb 6, 2024

urkud reviewed Feb 11, 2024

View reviewed changes

Mathlib/Data/Set/Intervals/Disjoint.lean Outdated Show resolved Hide resolved

urkud reviewed Feb 11, 2024

View reviewed changes

urkud added awaiting-author A reviewer has asked the author a question or requested changes t-order Order hierarchy and removed awaiting-review The author would like community review of the PR labels Feb 11, 2024

mo271 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 Feb 12, 2024

mo271 force-pushed the mo271/union_inter_bdd branch from ac2a85d to dd3f397 Compare February 16, 2024 13:01

mo271 mentioned this pull request Feb 16, 2024

[Merged by Bors] - chore(Probability/Kernel/CondCdf): cleanup #10635

Closed

1 task

This was referenced Mar 22, 2024

[Merged by Bors] - refactor: use CdfToKernel in CondCdf #11529

Closed

chore: move Real.iUnion_Iic_rat/iInter_Iic_rat #11638

Closed

RemyDegenne requested a review from urkud March 25, 2024 09:50

RemyDegenne approved these changes Mar 26, 2024

View reviewed changes

Mathlib/Data/Set/Intervals/Disjoint.lean Outdated Show resolved Hide resolved

Mathlib/Data/Set/Intervals/Disjoint.lean Outdated Show resolved Hide resolved

leanprover-community-mathlib4-bot added delegated and removed awaiting-review The author would like community review of the PR labels Mar 26, 2024

mathlib-bors bot pushed a commit that referenced this pull request Mar 26, 2024

feat(Data/Set/Intervals/Disjoint): i[Inter|Union]_Ii[c|o]... (#10298)

d6e8650

Co-authored-by: Moritz Firsching <firsching@google.com>

mo271 and others added 5 commits March 26, 2024 13:58

feat(Data/Set/Intervals/Disjoint): i[Inter|Union]_Ii[c|o]...

b363f09

review comments

d6f979a

rename

e480a88

Update Mathlib/Data/Set/Intervals/Disjoint.lean

9e84f37

Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

Update Mathlib/Data/Set/Intervals/Disjoint.lean

5407d43

Co-authored-by: Rémy Degenne <remydegenne@gmail.com>

fix build

0599398

mo271 force-pushed the mo271/union_inter_bdd branch from e29b9c7 to 0599398 Compare March 26, 2024 13:04

mathlib-bors bot pushed a commit that referenced this pull request Mar 26, 2024

feat(Data/Set/Intervals/Disjoint): i[Inter|Union]_Ii[c|o]... (#10298)

7866069

Co-authored-by: Moritz Firsching <firsching@google.com>

mathlib-bors bot changed the title ~~feat(Data/Set/Intervals/Disjoint): i[Inter|Union]_Ii[c|o]...~~ [Merged by Bors] - feat(Data/Set/Intervals/Disjoint): i[Inter|Union]_Ii[c|o]... Mar 26, 2024

mathlib-bors bot closed this Mar 26, 2024

mathlib-bors bot deleted the mo271/union_inter_bdd branch March 26, 2024 16:32

mathlib-bors bot pushed a commit that referenced this pull request Mar 27, 2024

chore(Probability/Kernel/CondCdf): cleanup (#10635)

59a00af

- [x] depends on: #10298 Co-authored-by: Moritz Firsching <firsching@google.com>

Louddy pushed a commit that referenced this pull request Apr 15, 2024

feat(Data/Set/Intervals/Disjoint): i[Inter|Union]_Ii[c|o]... (#10298)

caed720

Co-authored-by: Moritz Firsching <firsching@google.com>

Louddy pushed a commit that referenced this pull request Apr 15, 2024

chore(Probability/Kernel/CondCdf): cleanup (#10635)

a7d95a7

- [x] depends on: #10298 Co-authored-by: Moritz Firsching <firsching@google.com>

atarnoam pushed a commit that referenced this pull request Apr 16, 2024

feat(Data/Set/Intervals/Disjoint): i[Inter|Union]_Ii[c|o]... (#10298)

e061172

Co-authored-by: Moritz Firsching <firsching@google.com>

atarnoam pushed a commit that referenced this pull request Apr 16, 2024

chore(Probability/Kernel/CondCdf): cleanup (#10635)

6ac19aa

- [x] depends on: #10298 Co-authored-by: Moritz Firsching <firsching@google.com>

uniwuni pushed a commit that referenced this pull request Apr 19, 2024

feat(Data/Set/Intervals/Disjoint): i[Inter|Union]_Ii[c|o]... (#10298)

a2b6b4f

Co-authored-by: Moritz Firsching <firsching@google.com>

uniwuni pushed a commit that referenced this pull request Apr 19, 2024

chore(Probability/Kernel/CondCdf): cleanup (#10635)

1dbc0b2

- [x] depends on: #10298 Co-authored-by: Moritz Firsching <firsching@google.com>

callesonne pushed a commit that referenced this pull request Apr 22, 2024

feat(Data/Set/Intervals/Disjoint): i[Inter|Union]_Ii[c|o]... (#10298)

49e441a

Co-authored-by: Moritz Firsching <firsching@google.com>

callesonne pushed a commit that referenced this pull request Apr 22, 2024

chore(Probability/Kernel/CondCdf): cleanup (#10635)

3f80110

- [x] depends on: #10298 Co-authored-by: Moritz Firsching <firsching@google.com>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(Data/Set/Intervals/Disjoint): i[Inter|Union]_Ii[c|o]... #10298

[Merged by Bors] - feat(Data/Set/Intervals/Disjoint): i[Inter|Union]_Ii[c|o]... #10298

mo271 commented Feb 6, 2024

mo271 commented Feb 6, 2024

urkud Feb 11, 2024

mo271 Feb 12, 2024

mo271 Mar 5, 2024

urkud Feb 11, 2024

mo271 Feb 12, 2024

RemyDegenne left a comment

mathlib-bors bot commented Mar 26, 2024

mo271 commented Mar 26, 2024

mathlib-bors bot commented Mar 26, 2024

mo271 commented Mar 26, 2024

mathlib-bors bot commented Mar 26, 2024

mo271 commented Mar 26, 2024

mo271 commented Mar 26, 2024

mathlib-bors bot commented Mar 26, 2024

[Merged by Bors] - feat(Data/Set/Intervals/Disjoint): i[Inter|Union]_Ii[c|o]... #10298

[Merged by Bors] - feat(Data/Set/Intervals/Disjoint): i[Inter|Union]_Ii[c|o]... #10298

Conversation

mo271 commented Feb 6, 2024

mo271 commented Feb 6, 2024

urkud Feb 11, 2024

Choose a reason for hiding this comment

mo271 Feb 12, 2024

Choose a reason for hiding this comment

mo271 Mar 5, 2024

Choose a reason for hiding this comment

urkud Feb 11, 2024

Choose a reason for hiding this comment

mo271 Feb 12, 2024

Choose a reason for hiding this comment

RemyDegenne left a comment

Choose a reason for hiding this comment

mathlib-bors bot commented Mar 26, 2024

mo271 commented Mar 26, 2024

mathlib-bors bot commented Mar 26, 2024

mo271 commented Mar 26, 2024

mathlib-bors bot commented Mar 26, 2024

mo271 commented Mar 26, 2024

mo271 commented Mar 26, 2024

mathlib-bors bot commented Mar 26, 2024