-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(Analysis/LocallyConvex/WithSeminorms): congr lemmas #5797
Conversation
This PR/issue depends on: |
@@ -628,7 +627,7 @@ theorem continuous_iff_continuous_comp {q : SeminormFamily 𝕜₂ F ι'} [Topol | |||
#align seminorm.continuous_iff_continuous_comp Seminorm.continuous_iff_continuous_comp | |||
|
|||
theorem continuous_from_bounded {p : SeminormFamily 𝕝 E ι} {q : SeminormFamily 𝕝₂ F ι'} | |||
[TopologicalSpace E] (hp : WithSeminorms p) [TopologicalSpace F] (hq : WithSeminorms q) | |||
{_ : TopologicalSpace E} (hp : WithSeminorms p) {_ : TopologicalSpace F} (hq : WithSeminorms q) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What's the reason for this change?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
With the old version this line doesn't work. More generally, I feel like everything goes way smoother when things that can be inferred from various places (these topologies can either be inferred from the expected type or from the types of the arguments) aren't also searched by the typeclass system, especially since Lean4 seems to be even more strict on that than Lean3.
variable [NormedField 𝕜₂] [AddCommGroup F] [Module 𝕜₂ F] | ||
variable {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] | ||
|
||
protected theorem congr {p : SeminormFamily 𝕜 E ι} {q : SeminormFamily 𝕜 E ι'} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe add a docstring to this one.
bors r+ |
This adds `WithSeminorms.congr` which allows to replace a family of seminorm by an equivalent one. We use that to prove that one can always replace the family by a directed family (and a nice one if the indexing set is a `LocallyFiniteOrderBot`).
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
This adds `WithSeminorms.congr` which allows to replace a family of seminorm by an equivalent one. We use that to prove that one can always replace the family by a directed family (and a nice one if the indexing set is a `LocallyFiniteOrderBot`).
This adds `WithSeminorms.congr` which allows to replace a family of seminorm by an equivalent one. We use that to prove that one can always replace the family by a directed family (and a nice one if the indexing set is a `LocallyFiniteOrderBot`).
This adds
WithSeminorms.congr
which allows to replace a family of seminorm by an equivalent one. We use that to prove that one can always replace the family by a directed family (and a nice one if the indexing set is aLocallyFiniteOrderBot
).