[Merged by Bors] - feat: SeparatelyContinuousMul class for multiplication which is continuous in each variable#35589
Closed
j-loreaux wants to merge 8 commits intoleanprover-community:masterfrom
Closed
Conversation
…tinuous in each variable
github-actions
bot
added
the
t-topology
PR summary 08657ed7f8Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
Contributor
|
✌️ j-loreaux can now approve this pull request. To approve and merge a pull request, simply reply with |
mathlib-triage
bot
added
the
delegated
Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
Contributor
Author
|
bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Feb 26, 2026
…tinuous in each variable (#35589) In functional analysis, more specifically operator algebras, one often considers topologies weaker than the norm topology. There are a plethora of these, and virtually none of them satisfy docs#ContinuousMul because multiplication is not jointly continuous, but it *is* continuous in each variable separately. Sometimes multiplication is jointly continuous on bounded sets. In fact, this separate continuity of multiplication is really the correct hypothesis for a bunch of places where we use `ContinuousMul`. E.g., it is the proper assumption for docs#Set.isClosed_centralizer, but it's also the correct one for working with topological subobjects. Of course, one way to spell this separate continuity is `ContinuousConstSMul α α` and `ContinuousConstSMul αᵐᵒᵖ α`, but this is painful because it means (a) you need to write down both classes whenever you want to prove something about it, and (b) all the generic lemmas are about `•` instead of `*`. Consequently, in this PR we define classes `SeparatelyContinuousMul` (and `SeparatelyContinuousAdd` via `to_additive`) to encode this weaker form of continuity of multiplication.
Contributor
|
Pull request successfully merged into master. Build succeeded:
|
mathlib-bors
bot
changed the title
SeparatelyContinuousMul class for multiplication which is continuous in each variableSeparatelyContinuousMul class for multiplication which is continuous in each variable
pfaffelh
pushed a commit
to pfaffelh/mathlib4
that referenced
this pull request
Mar 2, 2026
…tinuous in each variable (leanprover-community#35589) In functional analysis, more specifically operator algebras, one often considers topologies weaker than the norm topology. There are a plethora of these, and virtually none of them satisfy docs#ContinuousMul because multiplication is not jointly continuous, but it *is* continuous in each variable separately. Sometimes multiplication is jointly continuous on bounded sets. In fact, this separate continuity of multiplication is really the correct hypothesis for a bunch of places where we use `ContinuousMul`. E.g., it is the proper assumption for docs#Set.isClosed_centralizer, but it's also the correct one for working with topological subobjects. Of course, one way to spell this separate continuity is `ContinuousConstSMul α α` and `ContinuousConstSMul αᵐᵒᵖ α`, but this is painful because it means (a) you need to write down both classes whenever you want to prove something about it, and (b) all the generic lemmas are about `•` instead of `*`. Consequently, in this PR we define classes `SeparatelyContinuousMul` (and `SeparatelyContinuousAdd` via `to_additive`) to encode this weaker form of continuity of multiplication.
pevogam
pushed a commit
to pevogam/mathlib4
that referenced
this pull request
Mar 19, 2026
…tinuous in each variable (leanprover-community#35589) In functional analysis, more specifically operator algebras, one often considers topologies weaker than the norm topology. There are a plethora of these, and virtually none of them satisfy docs#ContinuousMul because multiplication is not jointly continuous, but it *is* continuous in each variable separately. Sometimes multiplication is jointly continuous on bounded sets. In fact, this separate continuity of multiplication is really the correct hypothesis for a bunch of places where we use `ContinuousMul`. E.g., it is the proper assumption for docs#Set.isClosed_centralizer, but it's also the correct one for working with topological subobjects. Of course, one way to spell this separate continuity is `ContinuousConstSMul α α` and `ContinuousConstSMul αᵐᵒᵖ α`, but this is painful because it means (a) you need to write down both classes whenever you want to prove something about it, and (b) all the generic lemmas are about `•` instead of `*`. Consequently, in this PR we define classes `SeparatelyContinuousMul` (and `SeparatelyContinuousAdd` via `to_additive`) to encode this weaker form of continuity of multiplication.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
In functional analysis, more specifically operator algebras, one often considers topologies weaker than the norm topology. There are a plethora of these, and virtually none of them satisfy docs#ContinuousMul because multiplication is not jointly continuous, but it is continuous in each variable separately. Sometimes multiplication is jointly continuous on bounded sets.
In fact, this separate continuity of multiplication is really the correct hypothesis for a bunch of places where we use
ContinuousMul. E.g., it is the proper assumption for docs#Set.isClosed_centralizer, but it's also the correct one for working with topological subobjects. Of course, one way to spell this separate continuity isContinuousConstSMul α αandContinuousConstSMul αᵐᵒᵖ α, but this is painful because it means (a) you need to write down both classes whenever you want to prove something about it, and (b) all the generic lemmas are about•instead of*.Consequently, in this PR we define classes
SeparatelyContinuousMul(andSeparatelyContinuousAddviato_additive) to encode this weaker form of continuity of multiplication.I've only done a limited amount of generalization here for
SubsemigroupandSubmonoid, just to show that the basic material generalizes. In a follow-up PR I will do more generalization using this class.