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(topology/[separation, dense_embedding]): a function to a T1 space which has a limit at x is continuous at x #9934
Conversation
@@ -125,10 +125,26 @@ lemma extend_eq_at [t2_space γ] {f : α → γ} (a : α) (hf : continuous_at f | |||
di.extend f (i a) = f a := |
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.
Looking at this line now, it feels weird than a
is an explicit argument. If you have patience, could you try to make it implicit and see whether this needs @
down the road?
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.
Done ! (Unless I missed some occurrence of this lemma)
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
LGTM |
…e which has a limit at x is continuous at x (#9934) We prove that, for a function `f` with values in a T1 space, knowing that `f` admits *any* limit at `x` suffices to prove that `f` is continuous at `x`. We then use it to give a variant of `dense_inducing.extend_eq` with the same assumption required for continuity of the extension, which makes using both `extend_eq` and `continuous_extend` easier, and also brings us closer to Bourbaki who makes no explicit continuity assumption on the function to extend.
Pull request successfully merged into master. Build succeeded: |
…e which has a limit at x is continuous at x (#9934) We prove that, for a function `f` with values in a T1 space, knowing that `f` admits *any* limit at `x` suffices to prove that `f` is continuous at `x`. We then use it to give a variant of `dense_inducing.extend_eq` with the same assumption required for continuity of the extension, which makes using both `extend_eq` and `continuous_extend` easier, and also brings us closer to Bourbaki who makes no explicit continuity assumption on the function to extend.
We prove that, for a function
f
with values in a T1 space, knowing thatf
admits any limit atx
suffices to prove thatf
is continuous atx
.We then use it to give a variant of
dense_inducing.extend_eq
with the same assumption required for continuity of the extension, which makes using bothextend_eq
andcontinuous_extend
easier, and also brings us closer to Bourbaki who makes no explicit continuity assumption on the function to extend.