Zulip Chat Archive

Stream: maths

Topic: a small topology lemma


Matias Heikkilä (Apr 15 2022 at 18:41):

A tiny PR: https://github.com/leanprover-community/mathlib/pull/13469

What do you think? While this is quite trivial given continuous.ext_on, I'd personally expect this to be stated explicitly near the existence lemma continuous_stone_cech_extend.

Yaël Dillies (Apr 15 2022 at 18:42):

For boring technical reasons, you will have to close this PR and reopen one from the mathlib repository. Can a @maintainers give Matias write access?

Matias Heikkilä (Apr 15 2022 at 18:43):

oh I have it, sorry thought I needed to fork

Matias Heikkilä (Apr 15 2022 at 18:43):

just a sec

Matias Heikkilä (Apr 15 2022 at 18:48):

https://github.com/leanprover-community/mathlib/pull/13472


Last updated: Dec 20 2023 at 11:08 UTC