[Merged by Bors] - feat(Topology/Sublevel): sublevels in relation with semicontinuity and compactness by AntoineChambert-Loir · Pull Request #31558 · leanprover-community/mathlib4

AntoineChambert-Loir · 2025-11-12T16:14:11Z

Two lemmas about sublevels and semicontinuity related to compactness

Set.isCompact_inter_preimage_Iic, the sublevels of a lower semicontinuous function on a compact set are compact.
Set.biInter_sep_map_le_eq_empty_iff_exists_finset, an intersection of sublevel sets of a lower semicontinuous function on a compact set is empty if and only if a finite sub-intersection is already empty.

Co-authored with @ADedecker

github-actions · 2025-11-12T16:15:23Z

PR summary 64c4b4691e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ IsCompact.elim_finite_subfamily_isClosed_subtype
+ LowerSemicontinuousOn.inter_biInter_preimage_Iic_eq_empty_iff_exists_finset
+ LowerSemicontinuousOn.isCompact_inter_preimage_Iic
+ UpperSemicontinuousOn.inter_biInter_preimage_Ici_eq_empty_iff_exists_finset
+ UpperSemicontinuousOn.isCompact_inter_preimage_Ici

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.

No changes to technical debt.

You can run this locally as

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

j-loreaux

This is an initial pass. There's a lot of minor things to fix. After those are handled I will have a more detailed look.

I'm not saying it's unreasonable to have these, but can you say a bit about why you want them? And have you considered whether or not they should be abbrevs?

…hlib4 into ACLAD-Sublevels

mathlib4-merge-conflict-bot · 2025-11-19T09:38:16Z

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

j-loreaux · 2025-11-25T15:22:49Z

I'm not saying it's unreasonable to have these, but can you say a bit about why you want them? And have you considered whether or not they should be abbrevs?

This was never addressed, can you please do so?

j-loreaux

Please also update the PR description

Co-authored-by: Jireh Loreaux <[email protected]>

AntoineChambert-Loir · 2025-11-29T10:51:02Z

If the Semicontinuous file were not that big, these two lemmas could have been hosted there.

j-loreaux

We generally don't do things only for the lower versions, can you please add the upper versions too?

j-loreaux · 2025-12-02T16:02:23Z

If the Semicontinuous file were not that big, these two lemmas could have been hosted there.

I have a plan to split that file anyway, and with these golfs it might fit there. Can you please move these results there?

Co-authored-by: Jireh Loreaux <[email protected]>

j-loreaux

Thanks!

bors d+

j-loreaux · 2025-12-09T15:26:46Z


 alias ⟨LowerSemicontinuous.isClosed_epigraph, _⟩ := lowerSemicontinuous_iff_isClosed_epigraph

+omit [TopologicalSpace γ] in


Instead of omit [TopologicalSpace γ] in, can you instead just jump up to the variable invocation and split it into a mini section, as in:

variable {γ : Type*} [LinearOrder γ] [TopologicalSpace γ] [ClosedIciTopology γ]

becomes

variable {γ : Type*} [LinearOrder γ] section variable [TopologicalSpace γ] [ClosedIciTopology γ] -- the next few results which need this end

mathlib-bors · 2025-12-09T15:27:15Z

✌️ AntoineChambert-Loir can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

AntoineChambert-Loir · 2025-12-09T17:26:58Z

bors r+

@ADedecker

…d compactness (#31558) Two lemmas about sublevels and semicontinuity related to compactness * `Set.isCompact_inter_preimage_Iic`, the sublevels of a lower semicontinuous function on a compact set are compact. * `Set.biInter_sep_map_le_eq_empty_iff_exists_finset`, an intersection of sublevel sets of a lower semicontinuous function on a compact set is empty if and only if a finite sub-intersection is already empty. Co-authored with @ADedecker

mathlib-bors · 2025-12-09T18:53:09Z

Pull request successfully merged into master.

Build succeeded:

AntoineChambert-Loir added 3 commits November 12, 2025 16:59

initial commit

52c3330

add file in Mathlib.lean

aa8bd48

initial commit

5c79bd4

github-actions bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Nov 12, 2025

adjust docstring

46afc76

AntoineChambert-Loir mentioned this pull request Nov 12, 2025

[Merged by Bors] - feat(Topology/Sion): the minimax theorem of von Neumann - Sion #31560

Closed

3 tasks

AntoineChambert-Loir added 2 commits November 12, 2025 18:33

Merge branch 'master' into ACLAD-Sublevels

c6928c6

upate Mathlib.lean

4d86f22

leanprover-community-bot-assistant assigned j-loreaux Nov 16, 2025

j-loreaux reviewed Nov 18, 2025

View reviewed changes

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 18, 2025

AntoineChambert-Loir added 3 commits November 18, 2025 22:06

Merge branch 'master' into ACLAD-Sublevels

3b7e36b

adjust after first comments

9a2256a

Merge branch 'ACLAD-Sublevels' of github.com:AntoineChambert-Loir/mat…

2f3e5b7

…hlib4 into ACLAD-Sublevels

AntoineChambert-Loir removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 19, 2025

mathlib4-merge-conflict-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 Nov 19, 2025

Merge branch 'master' into ACLAD-Sublevels

44e51c5

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 Nov 19, 2025

AntoineChambert-Loir added 3 commits November 20, 2025 20:55

update Mathlib.lean

fff9498

Merge branch 'master' into ACLAD-Sublevels

2a3e009

adjust

7912152

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 25, 2025

dégraissage brutal

1781382

AntoineChambert-Loir changed the title ~~feat(Topology/Sublevel): sublevels and overlevels, relation with semicontinuity~~ feat(Topology/Sublevel): sublevels in relation with semicontinuity and compactness Nov 26, 2025

AntoineChambert-Loir removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 26, 2025

j-loreaux reviewed Nov 27, 2025

View reviewed changes

Comment thread Mathlib/Topology/Compactness/Compact.lean Outdated

Comment thread Mathlib/Topology/Sublevel.lean Outdated

Comment thread Mathlib/Topology/Sublevel.lean Outdated

Comment thread Mathlib/Topology/Sublevel.lean Outdated

Comment thread Mathlib/Topology/Sublevel.lean Outdated

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 27, 2025

AntoineChambert-Loir and others added 2 commits November 29, 2025 11:41

Apply suggestions from code review

f1d5aa4

Co-authored-by: Jireh Loreaux <[email protected]>

adjust after review

a5f9126

Merge branch 'master' into ACLAD-Sublevels

0cec460

AntoineChambert-Loir removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 29, 2025

j-loreaux reviewed Dec 2, 2025

View reviewed changes

Comment thread Mathlib/Topology/Sublevel.lean Outdated

Comment thread Mathlib/Topology/Sublevel.lean Outdated

Comment thread Mathlib/Topology/Compactness/Compact.lean Outdated

Comment thread Mathlib/Topology/Sublevel.lean Outdated

Comment thread Mathlib/Topology/Sublevel.lean Outdated

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 2, 2025

AntoineChambert-Loir and others added 3 commits December 3, 2025 09:20

Apply suggestions from code review

217215e

Co-authored-by: Jireh Loreaux <[email protected]>

adjust, create upper version, mv to semicontinuous file

4431fc2

Merge branch 'master' into ACLAD-Sublevels

93915af

AntoineChambert-Loir removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 5, 2025

j-loreaux reviewed Dec 9, 2025

View reviewed changes

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Dec 9, 2025

isolate topological results in a section

bf61f22

mathlib-bors bot changed the title ~~feat(Topology/Sublevel): sublevels in relation with semicontinuity and compactness~~ [Merged by Bors] - feat(Topology/Sublevel): sublevels in relation with semicontinuity and compactness Dec 9, 2025

mathlib-bors bot closed this Dec 9, 2025


		alias ⟨LowerSemicontinuous.isClosed_epigraph, _⟩ := lowerSemicontinuous_iff_isClosed_epigraph

		omit [TopologicalSpace γ] in

Conversation

AntoineChambert-Loir commented Nov 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Nov 12, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 64c4b4691e

Import changes for modified files

Declarations diff

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

j-loreaux commented Nov 25, 2025

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

AntoineChambert-Loir commented Nov 29, 2025

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

j-loreaux commented Dec 2, 2025

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

j-loreaux Dec 9, 2025

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Dec 9, 2025

Uh oh!

AntoineChambert-Loir commented Dec 9, 2025

Uh oh!

mathlib-bors bot commented Dec 9, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

AntoineChambert-Loir commented Nov 12, 2025 •

edited

Loading

github-actions bot commented Nov 12, 2025 •

edited

Loading