is_open {true}

Stream: maths

[Chris Hughes]

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

[Chris Hughes]

The topology on Prop is generate_from {true}

[Sebastien Gouezel]

library_search says exact is_open_discrete {to_bool true}

[Sebastien Gouezel]

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

[Sebastien Gouezel]

simp also works, by the way.

[Jesse Michael Han]

MWE:

import topology.order

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

[Jesse Michael Han]

but that lemma is just a thin wrapper around

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