Zulip Chat Archive

Stream: maths

Topic: is_open {true}


view this post on Zulip Chris Hughes (May 16 2019 at 19:33):

how to prove is_open {true}? This should be very easy.

view this post on Zulip Chris Hughes (May 16 2019 at 19:33):

The topology on Prop is generate_from {true}

view this post on Zulip Sebastien Gouezel (May 16 2019 at 19:48):

library_search says exact is_open_discrete {to_bool true}

view this post on Zulip Sebastien Gouezel (May 16 2019 at 19:49):

Sorry, my message is for true in bool. In Prop, library_search says exact is_open_singleton_true.

view this post on Zulip Sebastien Gouezel (May 16 2019 at 19:51):

simp also works, by the way.

view this post on Zulip Jesse Michael Han (May 16 2019 at 20:01):

MWE:

import topology.order

example : is_open ({true} : set Prop) :=  is_open_singleton_true

view this post on Zulip Jesse Michael Han (May 16 2019 at 20:05):

but that lemma is just a thin wrapper around

example : is_open ({true} : set Prop) :=
generate_open.basic _ (by exact or.inl rfl)

Last updated: May 12 2021 at 07:17 UTC