Urysohn's Lemma?

Stream: Is there code for X?

[Christopher Hoskin]

Has Urysohn's Lemma been proved in Lean? https://en.wikipedia.org/wiki/Urysohn%27s_lemma Thanks.

[Kevin Buzzard]

Doesn't look like it, in the sense that searching mathlib doesn't show up anything. All the ingredients are there though, so it would certainly be possible. Perhaps it might already be on someone's radar though so it's good to ask here.

[Reid Barton]

I have a proof lying around somewhere

[Christopher Hoskin]

@Reid Barton I would have thought that would be worth including in Mathlib, as it's frequently used in topology.

[Johan Commelin]

@Christopher Hoskin it certainly is... but sometimes you write more lean code then you end up making PRs for...

[Yury G. Kudryashov]

#6967