Skip to content

[Merged by Bors] - feat(Topology): the partition of a space into fibers of a function#15527

Closed
dagurtomas wants to merge 7 commits intomasterfrom
dagur/FiberPartition
Closed

[Merged by Bors] - feat(Topology): the partition of a space into fibers of a function#15527
dagurtomas wants to merge 7 commits intomasterfrom
dagur/FiberPartition

Conversation

@dagurtomas
Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas commented Aug 5, 2024

On its own this PR may seem strange, but this API is useful in #15321 to prove that discrete condensed sets are given by locally constant maps.

Open in Gitpod

@dagurtomas dagurtomas added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Aug 5, 2024
@dagurtomas dagurtomas mentioned this pull request Aug 5, 2024
Closed
4 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 5, 2024 •
edited
Loading

PR summary cefd72ff57

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Logic.Function.FiberPartition 212
Mathlib.Topology.FiberPartition 680

Declarations diff

+ Fiber
+ eq_fiber_image
+ fiber_nonempty
+ image
+ image_eq_image_mk
+ instance (x : Fiber l) : CompactSpace x.val := by
+ instance : Finite (Fiber l)
+ map_eq_image
+ map_preimage_eq_image
+ map_preimage_eq_image_map
+ mem_iff_eq_image
+ mk
+ mkSelf
+ mk_image
+ preimage
+ sigmaIncl
+ sigmaInclIncl
+ sigmaIsoHom
+ sigmaIsoHom_inj
+ sigmaIsoHom_surj

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

jcommelin
jcommelin reviewed Aug 12, 2024
View reviewed changes
dagurtomas and others added 2 commits August 12, 2024 15:04
@dagurtomas @jcommelin
Update Mathlib/Logic/Function/FiberPartition.lean
40c048f 
Co-authored-by: Johan Commelin <johan@commelin.net>
@dagurtomas
fibers_nonempty
63a9824
YaelDillies
YaelDillies reviewed Sep 5, 2024
View reviewed changes
dagurtomas and others added 2 commits September 5, 2024 09:50
@dagurtomas @YaelDillies
Update Mathlib/Logic/Function/FiberPartition.lean
1586dcb 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@dagurtomas
Fibers->Fiber
f541c5a
@YaelDillies YaelDillies requested a review from sgouezel September 6, 2024 14:54
jcommelin
jcommelin reviewed Sep 19, 2024
View reviewed changes
Copy link
Copy Markdown
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

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Sep 19, 2024
mathlib-bors bot pushed a commit that referenced this pull request Sep 19, 2024
@dagurtomas
feat(Topology): the partition of a space into fibers of a function (#…
b359218 
…15527)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 19, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Topology): the partition of a space into fibers of a function [Merged by Bors] - feat(Topology): the partition of a space into fibers of a function Sep 19, 2024
@mathlib-bors mathlib-bors bot closed this Sep 19, 2024
@mathlib-bors mathlib-bors bot deleted the dagur/FiberPartition branch September 19, 2024 12:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@YaelDillies YaelDillies YaelDillies left review comments

@sgouezel sgouezel Awaiting requested review from sgouezel

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.

3 participants

@dagurtomas @jcommelin @YaelDillies