Zulip Chat Archive

Stream: Is there code for X?

Topic: Urysohn's Lemma?


Christopher Hoskin (Jan 25 2021 at 18:25):

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

Kevin Buzzard (Jan 25 2021 at 18:27):

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 (Jan 25 2021 at 18:28):

I have a proof lying around somewhere

Christopher Hoskin (Jan 25 2021 at 20:08):

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

Johan Commelin (Jan 25 2021 at 20:13):

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

Yury G. Kudryashov (Mar 30 2021 at 21:18):

#6967


Last updated: Dec 20 2023 at 11:08 UTC