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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(Topology/Constructions): add continuous_bool_rng #10513

Closed
wants to merge 22 commits into from
Closed

[Merged by Bors] - feat(Topology/Constructions): add continuous_bool_rng #10513

wants to merge 22 commits into from

Conversation

urkud
Copy link
Member

@urkud urkud commented Feb 13, 2024

Provide continuity criteria for functions X → Bool
and, more generally, X → Y, where Y has discrete topology.

Cleaning up old branches.

Open in Gitpod

@urkud
Snapshot
45d32bb
@urkud
Merge branch 'master' into YK-cont-to-bool
ef7316f
@urkud
Merge commit 'c769b9d88f' into YK-cont-to-bool
289a38f
@urkud
Merge commit '93e2bebd1c' into YK-cont-to-bool
3a33929
@urkud
Merge commit 'a58dc4fe98' into YK-cont-to-bool
4712263
@urkud
Merge commit '1bacc4eed5' into YK-cont-to-bool
16a5ea6
@urkud
Merge commit 'f9c99994aa' into YK-cont-to-bool
70d00f3
@urkud
Merge commit 'fca1e12a79' into YK-cont-to-bool
2c1b80b
@urkud
Merge commit '57cf5ffa97' into YK-cont-to-bool
da90f0f
@urkud
Merge commit 'b0a6f35ec2' into YK-cont-to-bool
36bd1da
@urkud
Merge commit 'aa0957f16b' into YK-cont-to-bool
b07716d
@urkud
Merge commit '778f663aa6' into YK-cont-to-bool
c696925
@urkud
Merge commit '75641abe70' into YK-cont-to-bool
3ac645a
@urkud
Merge branch 'master' into YK-cont-to-bool
68d5477
@urkud
Update
24451e2
@urkud
Merge master into YK-cont-to-bool (using imerge)
07d78d9
@urkud
Fix
d11cdcd
@urkud
Sync
41fc025 
We already have `continuous_isLeft`/`continuous_isRight`
with shorter proofs.
@urkud urkud added awaiting-review The author would like community review of the PR t-topology Topological spaces, uniform spaces, metric spaces, filters awaiting-CI labels Feb 13, 2024
adomani
adomani approved these changes Feb 14, 2024
View reviewed changes
Mathlib/Topology/Constructions.lean Outdated Show resolved Hide resolved
Mathlib/Topology/Order.lean Outdated Show resolved Hide resolved
@urkud @adomani
Update Mathlib/Topology/Order.lean
5508a7f 
Co-authored-by: damiano <adomani@gmail.com>
@urkud urkud added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Feb 14, 2024
@urkud urkud removed the awaiting-author A reviewer has asked the author a question or requested changes label Feb 15, 2024
@urkud urkud added the awaiting-review The author would like community review of the PR label Feb 15, 2024
@urkud urkud requested a review from adomani February 15, 2024 02:04
@adomani
Copy link
Collaborator

adomani commented Feb 15, 2024

Thanks for the changes: I like the Bool lemmas!

maintainer merge

@adomani
Copy link
Collaborator

adomani commented Feb 15, 2024

maintainer merge

@github-actions GitHub Actions
Copy link

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

jcommelin
jcommelin approved these changes Feb 15, 2024
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Feb 15, 2024
mathlib-bors bot pushed a commit that referenced this pull request Feb 15, 2024
@urkud
feat(Topology/Constructions): add continuous_bool_rng (#10513)
c9a8b43 
Provide continuity criteria for functions `X → Bool`
and, more generally, `X → Y`, where `Y` has discrete topology.
@mathlib-bors
Copy link

mathlib-bors bot commented Feb 15, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Topology/Constructions): add continuous_bool_rng [Merged by Bors] - feat(Topology/Constructions): add continuous_bool_rng Feb 15, 2024
@mathlib-bors mathlib-bors bot closed this Feb 15, 2024
@mathlib-bors mathlib-bors bot deleted the YK-cont-to-bool branch February 15, 2024 07:38
riccardobrasca pushed a commit that referenced this pull request Feb 18, 2024
@urkud @riccardobrasca
feat(Topology/Constructions): add continuous_bool_rng (#10513)
14bc45f 
Provide continuity criteria for functions `X → Bool`
and, more generally, `X → Y`, where `Y` has discrete topology.
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@urkud @dagurtomas
feat(Topology/Constructions): add continuous_bool_rng (#10513)
fad9899 
Provide continuity criteria for functions `X → Bool`
and, more generally, `X → Y`, where `Y` has discrete topology.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin approved these changes

@adomani adomani Awaiting requested review from adomani

Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. t-topology Topological spaces, uniform spaces, metric spaces, filters
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@urkud @adomani @jcommelin @leanprover-community-mathlib4-bot