a small topology lemma

Stream: maths

[Matias Heikkilä]

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]

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ä]

oh I have it, sorry thought I needed to fork

[Matias Heikkilä]

just a sec

[Matias Heikkilä]

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