Skip to content

feat: a sequential and countably compact space is sequentially compact#36385

Open
CoolRmal wants to merge 41 commits intoleanprover-community:masterfrom
CoolRmal:sequential
Open

feat: a sequential and countably compact space is sequentially compact#36385
CoolRmal wants to merge 41 commits intoleanprover-community:masterfrom
CoolRmal:sequential

Conversation

@CoolRmal
Copy link
Copy Markdown
Contributor

@CoolRmal CoolRmal commented Mar 9, 2026 •
edited
Loading

The main result proved in this PR is that a sequential and countably compact space is sequentially compact. We also prove some lemmas:

  1. If f is an embedding, then A is sequentially compact iff f '' A is sequentially compact. This result is then used to show the equivalence of IsSeqCompact A and SeqCompactSpace A.
  2. If f is inducing, then A is countably compact iff f '' A is countably compact. This result is then used to show the equivalence of IsCountablyCompact A and CountablyCompactSpace A.
  3. If f converges and g is another function such that g x ∈ closure {f x} for all x, then g also converges.

Open in Gitpod

mike1729 and others added 23 commits February 19, 2026 10:39
@mike1729
Definition IsCountablyCompact.
74d45d5
@mike1729
characterization by countably generated filters.
fb42a3b
@mike1729
Proof of characterization by countable covers.
c11b1fa
@mike1729
isCountablyCompact_iff_infinite_subset_has_accPt
d0d6213
@mike1729
IsCountablyCompact.isCompact [SecondCountableTopology E]
3fc7506
@mike1729
IsCountablyCompact.isCompact [SecondCountableTopology E]
7e7343e
@mike1729
simp
b83d42f
@mike1729
simp
4530201
@mike1729
Docs.
db0f894
@CoolRmal
Update CountablyCompact.lean
bb5d2c4
@mike1729
Golf, simp, golf
c2d9dc4
@mike1729
small golf in isCountablyCompact_iff_countable_open_cover
3f6c21b
@mike1729
golf IsCountablyCompact.elim_finite_subcover_image
5cdc0b9
@mike1729
Improve docstrings
598e848
@mike1729
move mapClusterPt_atTop_iff_forall_mem_closure
2e28b37
@mike1729
Merge branch 'master' into countable-compactness
c8679f3
@mike1729
Change definition to filter based.
b771d48
@CoolRmal
code stype
ae6e106
@CoolRmal
simp only shouldn't be used to end a goal
adcb87f
@CoolRmal
draft
d4c4105
@CoolRmal
Update CountablyCompact.lean
73b784e
@CoolRmal
complete the proof
faeb971
@CoolRmal
reference
449f5a2
@github-actions
Copy link
Copy Markdown

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

PR summary 20c47e339c

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Subtype.isCountablyCompact_iff
+ Subtype.isSeqCompact_iff
+ Tendsto.specializes
+ Topology.IsEmbedding.isCountablyCompact_iff
+ Topology.IsEmbedding.isSeqCompact_iff
+ Topology.IsInducing.isCountablyCompact_iff
+ instance [SequentialSpace E] [CountablyCompactSpace E] :
+ isClosed_of_not_tendsto
+ isCountablyCompact_iff_countablyCompactSpace
+ isCountablyCompact_iff_isCountablyCompact_univ
+ isCountablyCompact_univ_iff
+ isSeqCompact_iff_isSeqCompact_univ
+ isSeqCompact_iff_seqCompactSpace
+ isSeqCompact_univ_iff

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).

@github-actions github-actions bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Mar 9, 2026
@mathlib-dependent-issues mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 9, 2026
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 28, 2026
@felixpernegger felixpernegger mentioned this pull request Mar 31, 2026
Merged
scholzhannah
scholzhannah reviewed Mar 31, 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.

Thanks for your PR! I have some style comments.

@j-loreaux j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 31, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 1, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Apr 1, 2026

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 2, 2026
@CoolRmal
Copy link
Copy Markdown
Contributor Author

CoolRmal commented Apr 2, 2026

-awaiting-author

@github-actions github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 2, 2026
scholzhannah
scholzhannah reviewed Apr 2, 2026
View reviewed changes
Mathlib/Topology/Compactness/CountablyCompact.lean
Comment on lines +202 to +203
theorem Topology.IsEmbedding.isCountablyCompact_iff {f : E → F} (hf : IsEmbedding f) :
IsCountablyCompact A ↔ IsCountablyCompact (f '' A) :=
Copy link
Copy Markdown
Collaborator

@scholzhannah scholzhannah Apr 2, 2026

Choose a reason for hiding this comment

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

This theorem is probably the wrong way around since I think you will most of the time want to rewrite from right to left. I think if you switch the order, you could make this a simp-lemma.

Copy link
Copy Markdown
Contributor Author

@CoolRmal CoolRmal Apr 2, 2026

Choose a reason for hiding this comment

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

I am not sure about whether we should switch the order and make them simp lemmas. These lemmas are analogues of Topology.IsEmbedding.isCompact_iff, Subtype.isCompact_iff, etc. and they are not simp lemmas.

Copy link
Copy Markdown
Member

@ADedecker ADedecker Apr 3, 2026

Choose a reason for hiding this comment

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

I agree with @CoolRmal here.

Mathlib/Topology/Compactness/CountablyCompact.lean
Comment on lines +206 to +212
theorem Subtype.isCountablyCompact_iff {p : E → Prop} {A : Set { x // p x }} :
IsCountablyCompact A ↔ IsCountablyCompact ((↑) '' A : Set E) :=
IsEmbedding.subtypeVal.isCountablyCompact_iff

theorem isCountablyCompact_iff_isCountablyCompact_univ :
IsCountablyCompact A ↔ IsCountablyCompact (univ : Set A) := by
rw [Subtype.isCountablyCompact_iff, image_univ, Subtype.range_coe]
Copy link
Copy Markdown
Collaborator

@scholzhannah scholzhannah Apr 2, 2026

Choose a reason for hiding this comment

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

The same thing as above applies to these two theorems.

Mathlib/Topology/Compactness/CountablyCompact.lean
Comment on lines +284 to +285
theorem Topology.IsEmbedding.isSeqCompact_iff {f : E → F} (hf : IsEmbedding f) :
IsSeqCompact A ↔ IsSeqCompact (f '' A) where
Copy link
Copy Markdown
Collaborator

@scholzhannah scholzhannah Apr 2, 2026

Choose a reason for hiding this comment

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

Same thing as above.

@scholzhannah scholzhannah added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 2, 2026
@CoolRmal
Copy link
Copy Markdown
Contributor Author

CoolRmal commented Apr 2, 2026

-awaiting-author

@github-actions github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 2, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 3, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Apr 3, 2026

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 3, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@ADedecker ADedecker ADedecker left review comments

+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.

6 participants

@CoolRmal @ADedecker @scholzhannah @j-loreaux @PatrickMassot @mike1729