Zulip Chat Archive

Stream: general

Topic: Pop quiz

Gabriel Ebner (Mar 27 2020 at 18:18):

What is wrong with these two lemmas:

@[simp] lemma subsingleton.is_open [subsingleton α] (s : set α) : is_open s :=
subsingleton.set_cases is_open_empty is_open_univ s

@[simp] lemma is_open_discrete [discrete_topology α] (s : set α) : is_open s :=
(discrete_topology.eq_bot α).symm ▸ trivial

Kevin Buzzard (Mar 27 2020 at 18:22):

They are both true so nothing is wrong with them.

Kevin Buzzard (Mar 27 2020 at 18:22):

(deleted)

Kevin Buzzard (Mar 27 2020 at 18:23):

~~do you mean is_open_univ?~~(now fixed)

Gabriel Ebner (Mar 27 2020 at 18:25):

Hint: it's not the proofs.

Kevin Buzzard (Mar 27 2020 at 18:25):

(deleted)

Johan Commelin (Mar 27 2020 at 18:27):

Hint: it's something with simp...

Gabriel Ebner (Mar 27 2020 at 18:27):

I'll add an instance [subsingleton A] : discrete_topology A then the first should follow from the second one.

Kevin Buzzard (Mar 27 2020 at 18:28):

Well they look pretty confluent to me

Gabriel Ebner (Mar 27 2020 at 18:29):

I've spent an hour looking at them before I figured it out. Apparently the second lemma removes the first one from the simp set because they have the same conclusion... lean#163

Last updated: Dec 20 2023 at 11:08 UTC