[Merged by Bors] - feat: add `forall_is{Open,Closed}_iff` #33624

j-loreaux · 2026-01-05T21:05:35Z

A predicate holds for all open (resp. closed) sets if and only if it holds for the interior (resp. closure) of any set.

github-actions · 2026-01-05T21:06:43Z

PR summary 8885835846

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ exists_isClosed_iff
+ exists_isOpen_iff
+ forall_isClosed_iff
+ forall_isOpen_iff

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

vihdzp · 2026-01-05T22:01:23Z

Can we have exists versions too?

Also, do we get anything by reframing these as induction/recursion lemmas? (to prove something for a closed set, it suffices to prove it for the closure of a set).

j-loreaux · 2026-01-05T22:18:58Z

Can we have exists versions too?

Done.

Also, do we get anything by reframing these as induction/recursion lemmas? (to prove something for a closed set, it suffices to prove it for the closure of a set).

🤷 I suspect that's not terribly useful. I only wrote these because I wanted them as rewrites.

ocfnash · 2026-01-06T14:52:09Z

Thanks!

bors merge

A predicate holds for all open (resp. closed) sets if and only if it holds for the interior (resp. closure) of any set.

mathlib-bors · 2026-01-06T15:55:40Z

Pull request successfully merged into master.

Build succeeded:

This adds some API for upper hemicontinuous functions, including their behavior under pointwise union or intersection, post-composition by the preimage of a closed embedding (actually, injectivity is not necessary), and the characterization in terms of the convergence of sequences. This is is useful for a forthcoming PR proving the upper hemicontinuity of the spectrum in Banach algebras. Analogous results of lower hemicontinuous functions are *not* included because they are not as easily obtained from their upper counterparts as is the case for upper/lower semicontinuity, and our downstream applications involve upper hemicontinuity alone. - [ ] depends on: #33623 - [ ] depends on: #33624 - [ ] depends on: #33625

If `A` is a (unital) Banach `𝕜`-algebra, then `spectrum 𝕜 : A → Set 𝕜` is upper hemicontinuous. Likewise, if `A` is a Banach `ℝ`-algebra, this holds for `spectrum ℝ≥0` as well. In addition, both of these results are true for non-unital Banach algebras replacing `spectrum` by `quasispectrum`. This is useful for providing some more convenience lemmas establishing continuity of the continuous functional calculus in the operator variable. - [ ] depends on: #33623 - [ ] depends on: #33624 - [ ] depends on: #33625 - [ ] depends on: #33626

…calculus in the operator variable (#33628) If `a : X → A` is continuous and `A` is a C⋆-algebra and `f` is continuous on a neighborhood of the union of the spectra of `a x`, then `fun x ↦ cfc f (a x)` is continuous (assuming that `a x` satisfies the relevant predicate for the continuous functional calculus). This is slightly weaker than our existing theorems for the continuity of the continuous functional calculus (compare with `Continuous.cfc`), but it is often easier to apply in practice. In particular, it uses upper hemicontinuity of the spectrum to automatically satisfy some of the hypotheses in `Continuous.cfc` at the cost of requiring a *neighborhood* (instead of just compact sets containing the spectra). Indeed, in #33617 we use this to establish continuity of common functions defined in terms of the continuous functional calculus, such as `CFC.log`, `CFC.nnrpow`, `CFC.rpow`, `CFC.sqrt` and `CFC.abs`. - [ ] depends on: #33623 - [ ] depends on: #33624 - [ ] depends on: #33625 - [ ] depends on: #33626 - [ ] depends on: #33627

…nal calculus (#33617) Proves that `CFC.log`, `CFC.nnrpow`, `CFC.rpow`, `CFC.sqrt` and `CFC.abs` are continuous (on appropriate subsets of `A`). - [ ] depends on: #33623 - [ ] depends on: #33624 - [ ] depends on: #33625 - [ ] depends on: #33626 - [ ] depends on: #33627 - [ ] depends on: #33628

…over-community#33627) If `A` is a (unital) Banach `𝕜`-algebra, then `spectrum 𝕜 : A → Set 𝕜` is upper hemicontinuous. Likewise, if `A` is a Banach `ℝ`-algebra, this holds for `spectrum ℝ≥0` as well. In addition, both of these results are true for non-unital Banach algebras replacing `spectrum` by `quasispectrum`. This is useful for providing some more convenience lemmas establishing continuity of the continuous functional calculus in the operator variable. - [ ] depends on: leanprover-community#33623 - [ ] depends on: leanprover-community#33624 - [ ] depends on: leanprover-community#33625 - [ ] depends on: leanprover-community#33626

…calculus in the operator variable (leanprover-community#33628) If `a : X → A` is continuous and `A` is a C⋆-algebra and `f` is continuous on a neighborhood of the union of the spectra of `a x`, then `fun x ↦ cfc f (a x)` is continuous (assuming that `a x` satisfies the relevant predicate for the continuous functional calculus). This is slightly weaker than our existing theorems for the continuity of the continuous functional calculus (compare with `Continuous.cfc`), but it is often easier to apply in practice. In particular, it uses upper hemicontinuity of the spectrum to automatically satisfy some of the hypotheses in `Continuous.cfc` at the cost of requiring a *neighborhood* (instead of just compact sets containing the spectra). Indeed, in leanprover-community#33617 we use this to establish continuity of common functions defined in terms of the continuous functional calculus, such as `CFC.log`, `CFC.nnrpow`, `CFC.rpow`, `CFC.sqrt` and `CFC.abs`. - [ ] depends on: leanprover-community#33623 - [ ] depends on: leanprover-community#33624 - [ ] depends on: leanprover-community#33625 - [ ] depends on: leanprover-community#33626 - [ ] depends on: leanprover-community#33627

…nal calculus (leanprover-community#33617) Proves that `CFC.log`, `CFC.nnrpow`, `CFC.rpow`, `CFC.sqrt` and `CFC.abs` are continuous (on appropriate subsets of `A`). - [ ] depends on: leanprover-community#33623 - [ ] depends on: leanprover-community#33624 - [ ] depends on: leanprover-community#33625 - [ ] depends on: leanprover-community#33626 - [ ] depends on: leanprover-community#33627 - [ ] depends on: leanprover-community#33628

A predicate holds for all open (resp. closed) sets if and only if it holds for the interior (resp. closure) of any set.

…ty#33626) This adds some API for upper hemicontinuous functions, including their behavior under pointwise union or intersection, post-composition by the preimage of a closed embedding (actually, injectivity is not necessary), and the characterization in terms of the convergence of sequences. This is is useful for a forthcoming PR proving the upper hemicontinuity of the spectrum in Banach algebras. Analogous results of lower hemicontinuous functions are *not* included because they are not as easily obtained from their upper counterparts as is the case for upper/lower semicontinuity, and our downstream applications involve upper hemicontinuity alone. - [ ] depends on: leanprover-community#33623 - [ ] depends on: leanprover-community#33624 - [ ] depends on: leanprover-community#33625

…over-community#33627) If `A` is a (unital) Banach `𝕜`-algebra, then `spectrum 𝕜 : A → Set 𝕜` is upper hemicontinuous. Likewise, if `A` is a Banach `ℝ`-algebra, this holds for `spectrum ℝ≥0` as well. In addition, both of these results are true for non-unital Banach algebras replacing `spectrum` by `quasispectrum`. This is useful for providing some more convenience lemmas establishing continuity of the continuous functional calculus in the operator variable. - [ ] depends on: leanprover-community#33623 - [ ] depends on: leanprover-community#33624 - [ ] depends on: leanprover-community#33625 - [ ] depends on: leanprover-community#33626

…calculus in the operator variable (leanprover-community#33628) If `a : X → A` is continuous and `A` is a C⋆-algebra and `f` is continuous on a neighborhood of the union of the spectra of `a x`, then `fun x ↦ cfc f (a x)` is continuous (assuming that `a x` satisfies the relevant predicate for the continuous functional calculus). This is slightly weaker than our existing theorems for the continuity of the continuous functional calculus (compare with `Continuous.cfc`), but it is often easier to apply in practice. In particular, it uses upper hemicontinuity of the spectrum to automatically satisfy some of the hypotheses in `Continuous.cfc` at the cost of requiring a *neighborhood* (instead of just compact sets containing the spectra). Indeed, in leanprover-community#33617 we use this to establish continuity of common functions defined in terms of the continuous functional calculus, such as `CFC.log`, `CFC.nnrpow`, `CFC.rpow`, `CFC.sqrt` and `CFC.abs`. - [ ] depends on: leanprover-community#33623 - [ ] depends on: leanprover-community#33624 - [ ] depends on: leanprover-community#33625 - [ ] depends on: leanprover-community#33626 - [ ] depends on: leanprover-community#33627

…nal calculus (leanprover-community#33617) Proves that `CFC.log`, `CFC.nnrpow`, `CFC.rpow`, `CFC.sqrt` and `CFC.abs` are continuous (on appropriate subsets of `A`). - [ ] depends on: leanprover-community#33623 - [ ] depends on: leanprover-community#33624 - [ ] depends on: leanprover-community#33625 - [ ] depends on: leanprover-community#33626 - [ ] depends on: leanprover-community#33627 - [ ] depends on: leanprover-community#33628

feat: add forall_is{Open,Closed}_iff

7b8ec88

j-loreaux added t-topology Topological spaces, uniform spaces, metric spaces, filters easy < 20s of review time. See the lifecycle page for guidelines. labels Jan 5, 2026

exists versions

d0fc136

vihdzp approved these changes Jan 5, 2026

View reviewed changes

leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Jan 6, 2026

mathlib-bors bot pushed a commit that referenced this pull request Jan 6, 2026

feat: add forall_is{Open,Closed}_iff (#33624)

4e52851

A predicate holds for all open (resp. closed) sets if and only if it holds for the interior (resp. closure) of any set.

mathlib-bors bot changed the title ~~feat: add forall_is{Open,Closed}_iff~~ [Merged by Bors] - feat: add forall_is{Open,Closed}_iff Jan 6, 2026

mathlib-bors bot closed this Jan 6, 2026

adomani mentioned this pull request Jan 16, 2026

feat: MiM PR report #15355

Open

goliath-klein pushed a commit to PrParadoxy/mathlib4 that referenced this pull request Jan 24, 2026

feat: add forall_is{Open,Closed}_iff (leanprover-community#33624)

fd5b284

A predicate holds for all open (resp. closed) sets if and only if it holds for the interior (resp. closure) of any set.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: add `forall_is{Open,Closed}_iff` #33624

[Merged by Bors] - feat: add `forall_is{Open,Closed}_iff` #33624

Uh oh!

j-loreaux commented Jan 5, 2026

Uh oh!

github-actions bot commented Jan 5, 2026 •

edited

Loading

Declarations diff

Uh oh!

vihdzp commented Jan 5, 2026

Uh oh!

j-loreaux commented Jan 5, 2026

Uh oh!

ocfnash commented Jan 6, 2026

Uh oh!

mathlib-bors bot commented Jan 6, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

[Merged by Bors] - feat: add forall_is{Open,Closed}_iff #33624

[Merged by Bors] - feat: add forall_is{Open,Closed}_iff #33624

Uh oh!

Conversation

j-loreaux commented Jan 5, 2026

Uh oh!

github-actions bot commented Jan 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 8885835846

Import changes for modified files

Declarations diff

Uh oh!

vihdzp commented Jan 5, 2026

Uh oh!

j-loreaux commented Jan 5, 2026

Uh oh!

ocfnash commented Jan 6, 2026

Uh oh!

mathlib-bors bot commented Jan 6, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

[Merged by Bors] - feat: add `forall_is{Open,Closed}_iff` #33624

[Merged by Bors] - feat: add `forall_is{Open,Closed}_iff` #33624

github-actions bot commented Jan 5, 2026 •

edited

Loading