Zulip Chat Archive
Stream: Is there code for X?
Topic: discrete bot
Johan Commelin (Feb 10 2021 at 15:22):
I couldn't find this in mathlib, which seems surprising
import topology.subset_properties
instance discrete_topology_bot {α : Type*} : @discrete_topology α ⊥ :=
{ eq_bot := rfl }
Johan Commelin (Feb 10 2021 at 21:36):
PRd in #6163
Last updated: Dec 20 2023 at 11:08 UTC