add itv_closureE, itv_interiorE, and helper lemmas#1848
add itv_closureE, itv_interiorE, and helper lemmas#1848t6s wants to merge 2 commits intomath-comp:masterfrom
itv_closureE, itv_interiorE, and helper lemmas#1848Conversation
| Definition is_endless_porderType {d} (T : porderType d) := | ||
| forall x : T, (exists y, y < x) /\ (exists y, x < y). | ||
|
|
||
| Definition is_dense_porderType {d} (T : porderType d) := |
There was a problem hiding this comment.
This might need to be related to the definition dense in topology_structure.v.
There was a problem hiding this comment.
Denseness of a subset in a topological space is a different notion, and there does not seem to be a unifying theory.
Cyril suggested that using a fully qualified name like Order.dense would suffice for differentiating these two
(creating a PR to mathcomp/order.v).
|
|
||
| Lemma setUitv1 a x : (a <= BLeft x)%O -> | ||
| [set` Interval a (BLeft x)] `|` [set x] = [set` Interval a (BRight x)]. | ||
| Let setUitv1_gen a x b : (a <= BLeft x)%O -> |
There was a problem hiding this comment.
This indeed looks like a generalization, so maybe it should not be a Let but a replacement for setUitv1. Doing this generalization in a small, preliminary PR (maybe containing also setDitv1r and setDitv1l) could simplify the review of this one.
There was a problem hiding this comment.
One bad thing about this generalization is that all use cases of setUitv1 and setU1itv in analysis master are
backwards rewriting, and adding another parameter b breaks them.
I will create a PR to clarify this issue, and possibly try to simplify the relevant proofs there.
| Section theory. | ||
| Local Open Scope order_scope. | ||
|
|
||
| Definition is_endless_porderType {d} (T : porderType d) := |
There was a problem hiding this comment.
Definitions need to be documented, but I guess you were planning to do it later.
There was a problem hiding this comment.
Did you consider using an HB.mixin for this property? Since, for example, numDomainType is an instance, that might simplify the presentation of later lemmas.
There was a problem hiding this comment.
Turning this part into a structure using HB is actually good.
I somehow thought that would not work, but let us see by trying it. I will update the code in that way.
2 participants
Motivation for this change
Reviewing PR #1674 , it was noticed that there is not much theory
connecting closure/interior operators and set-intervals.
This PR adds lemmas to amend that, especially
itv_interiorEanditv_closureEstating that the interior/closure of an interval is an open/closed interval respectively,
for intervals in
realFieldType.This should resolve the following comment:
https://github.com/math-comp/analysis/pull/1674/changes/BASE..34697b2642259157cd3678e64092864dcd0ca4ef#r2685444293
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Merge policy
As a rule of thumb:
all compile are preferentially merged into master.
Reminder to reviewers