Zulip Chat Archive

Stream: Is there code for X?

Topic: Urysohn's Lemma?


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jan 25 2021 at 18:28):

I have a proof lying around somewhere

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Yury G. Kudryashov (Mar 30 2021 at 21:18):

#6967


Last updated: May 07 2021 at 22:14 UTC