Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

duality between closure and interior #1366

Open
wants to merge 6 commits into
base: master
Choose a base branch
from

Conversation

t6s
Copy link
Member

@t6s t6s commented Oct 25, 2024

Motivation for this change

This PR adds some lemmas for the closure and interior operators that
are a basic part of the duality between these. This addition will serve
as an initial step towards the theory of regular open/closed sets.

Lemma closureC is modified since its original statement seemed not
conforming to the name.

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

@t6s t6s requested a review from zstone1 October 25, 2024 13:42
Qed.

Lemma interior_closure_idem (A : set T) :
interior (closure (interior (closure A))) = interior (closure A).
Copy link
Member

Choose a reason for hiding this comment

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

Quick thought: could the following definition be useful?

Definition idempotent_fun (U : Type) (f : U -> U) := f \o f =1 f.

Copy link
Member Author

Choose a reason for hiding this comment

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

Nice. Which file should it be put in?

Copy link
Contributor

Choose a reason for hiding this comment

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

(oh wow, mathcomp's existing idempotent f predicate means f x x = x and not f (f x) = f x. I am always surprised by that one.) mathcomp-extra is a suitable place for this, I think

Copy link
Member

Choose a reason for hiding this comment

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

ssrfun.v? so, I guess for us it means mathcomp_extra.v...

Copy link
Member

Choose a reason for hiding this comment

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

I am always surprised by that one.

so maybe we could propose to rename it to idempotent_op?

Copy link
Contributor

@zstone1 zstone1 left a comment

Choose a reason for hiding this comment

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

All looks good. I'm a bit surprised we didn't have some of this fundamental stuff before, so I'm glad to see you adding it.

@affeldt-aist
Copy link
Member

affeldt-aist commented Oct 25, 2024

Don't hesitate to use when you can. @yoshihiro503 worked hard on making it clickable in the online documentation (https://math-comp.github.io/analysis/htmldoc_1_6_0/index.html) ^_^

@t6s
Copy link
Member Author

t6s commented Oct 25, 2024

Don't hesitate to use when you can. @yoshihiro503 worked hard on making it clickable in the online documentation (https://math-comp.github.io/analysis/htmldoc_1_6_0/index.html) ^_^

The problem is, I cannot easily input that circle symbol. (Do you know any SKK keystroke for that?)
But anyway, I'll do some copy-pasting later.

@t6s
Copy link
Member Author

t6s commented Oct 25, 2024

idempotent_fun is added.
I have also introduced definitions regopen and regclosed to state generalized versions of the idempotent lemmas.
I am afraid that these names are not particularly good, but regular_open seems too long.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants