reduce dependencies in measurable_structure.v#1979
Conversation
affeldt-aist
force-pushed
the
measurable_structure_20260527
branch
from
8495d56 to
6fbaccd
Compare
|
This is really just reducing dependencies in |
| Qed. | ||
|
|
||
| Lemma bigcup_bigsetU_bigcup F : | ||
| \bigcup_k \big[setU/set0]_(i < k.+1) F i = \bigcup_k F k. |
There was a problem hiding this comment.
not about this PR itself, but why do lemmas around here have .+1 in the indexing for finite parts?
There was a problem hiding this comment.
bigcup_bigsetU_bigcup can indeed be changed but of course it like adding an empty set to the big union
so I am not sure it is interesting, what do you think at the look of the last commit?
If by "around" you mean the next lemma bigcup_mkord_ord, this is inherent to the use of inord.
|
One action in the CI is failing, complaining xfinmap is not found. What is xfinmap? |
hoheinzollern
left a comment
hoheinzollern
left a comment
There was a problem hiding this comment.
Other than the comment about notation, looks good.
| Definition bigcup2 T (A B : set T) : nat -> set T := | ||
| Definition sequence R := nat -> R. | ||
|
|
||
| Notation "R ^nat" := (sequence R) : type_scope. |
There was a problem hiding this comment.
why is this notation introduced here? isn't it part of mathcomp already?
There was a problem hiding this comment.
No, it is not part of mathcomp.
I am not sure it is going to make it to mathcomp soon because it is about sequences and their theory is really developed in MathComp-Analysis.
This is the reason why I haven't even thought of moving it to unstable.v (the staging area).
affeldt-aist
force-pushed
the
measurable_structure_20260527
branch
from
cf0a729 to
9d49866
Compare
3 participants
Motivation for this change
fyi @hoheinzollern
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Merge policy
As a rule of thumb:
all compile are preferentially merged into master.
Reminder to reviewers