Skip to content

feat(Topology/ClosedBases): TopologicalSpace.IsClosedBasis and TopologicalSpace.IsClosedSubbasis s#36954

Open
FMLJohn wants to merge 20 commits intoleanprover-community:masterfrom
FMLJohn:closed_bases
Open

feat(Topology/ClosedBases): TopologicalSpace.IsClosedBasis and TopologicalSpace.IsClosedSubbasis s#36954
FMLJohn wants to merge 20 commits intoleanprover-community:masterfrom
FMLJohn:closed_bases

Conversation

@FMLJohn
Copy link
Copy Markdown
Collaborator

@FMLJohn FMLJohn commented Mar 21, 2026 •
edited
Loading

In this pull request, I have defined closed bases and closed subbases of topologies, and proved some basic properties of them.

Main definitions

  • TopologicalSpace.IsClosedBasis s: A closed basis of a topological space α is a collection of closed sets s : Set (Set α) such that every closed subset of α can be written as an intersection of elements of s.
  • TopologicalSpace.IsClosedSubbasis s: Given a topological space α, s : Set (Set α) is a closed subbasis if the topology on α equals generateFrom { uᶜ | u ∈ s }.

Open in Gitpod

@FMLJohn FMLJohn added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Mar 21, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 21, 2026 •
edited
Loading

PR summary 84c74f5825

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Topology.ClosedBases (new file) 614

Declarations diff

+ IsClosedBasis
+ IsClosedBasis.closed_iff_eq_sInter
+ IsClosedBasis.isClosed
+ closed_subbasis_iff_isClosedBasis_sUnion
+ closed_subbasis_iff_isTopologicalBasis_sInter_compl
+ isClosedBasis_iff
+ isClosedBasis_iff_and
+ isClosedBasis_of_closed_subbasis_of_union
+ isClosed_of_closed_subbasis_of_mem
+ subbasis_iff_isTopologicalBasis_sInter

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

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

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

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@FMLJohn FMLJohn requested a review from erdOne March 21, 2026 16:54
scholzhannah
scholzhannah reviewed Apr 1, 2026
View reviewed changes
Copy link
Copy Markdown
Collaborator

@scholzhannah scholzhannah left a comment

Choose a reason for hiding this comment

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

Thank you for your PR! Bases of closed sets sound like something we would want in Mathlib. I have left a few comments.

@scholzhannah
Copy link
Copy Markdown
Collaborator

scholzhannah commented Apr 1, 2026

Also please move your explanation and the added definitions above the line in the PR description so that they will end up in the commit message.

@scholzhannah scholzhannah added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 1, 2026
FMLJohn and others added 14 commits April 2, 2026 14:07
@FMLJohn @scholzhannah
Update Mathlib/Topology/ClosedBases.lean
ea802f8 
Co-authored-by: Hannah Scholz <[email protected]>
@FMLJohn @scholzhannah
Update Mathlib/Topology/Bases.lean
1118e95 
Co-authored-by: Hannah Scholz <[email protected]>
@FMLJohn @scholzhannah
Update Mathlib/Topology/Bases.lean
3c7ac23 
Co-authored-by: Hannah Scholz <[email protected]>
@FMLJohn @scholzhannah
Update Mathlib/Topology/ClosedBases.lean
ee85210 
Co-authored-by: Hannah Scholz <[email protected]>
@FMLJohn @scholzhannah
Update Mathlib/Topology/ClosedBases.lean
09428c6 
Co-authored-by: Hannah Scholz <[email protected]>
@FMLJohn @scholzhannah
Update Mathlib/Topology/ClosedBases.lean
e653975 
Co-authored-by: Hannah Scholz <[email protected]>
@FMLJohn @scholzhannah
Update Mathlib/Topology/ClosedBases.lean
419b294 
Co-authored-by: Hannah Scholz <[email protected]>
@FMLJohn @scholzhannah
Update Mathlib/Topology/ClosedBases.lean
a5b4993 
Co-authored-by: Hannah Scholz <[email protected]>
@FMLJohn
edit
a4d145d
@FMLJohn
new docstring
d962b35
@FMLJohn
implicit
9b70a04
@FMLJohn
omit a definition
c86686e
@FMLJohn
Merge branch 'master' into closed_bases
d77056d
@FMLJohn
Merge branch 'master' into closed_bases
76563da
@FMLJohn FMLJohn removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 3, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@erdOne erdOne Awaiting requested review from erdOne

1 more reviewer

@scholzhannah scholzhannah scholzhannah left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@PatrickMassot PatrickMassot

Labels

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

@FMLJohn @scholzhannah @PatrickMassot