Instances related to the discrete topology #
We prove that the discrete topology is a first-countable topology, and is second-countable for an
encodable type. Also, in linear orders which are also pred_order
and succ_order
, the discrete
topology is the order topology.
When importing this file and data.nat.succ_pred
, the instances second_countable_topology ℕ
and order_topology ℕ
become available.
@[protected, instance]
def
discrete_topology.first_countable_topology
{α : Type u_1}
[topological_space α]
[discrete_topology α] :
@[protected, instance]
def
discrete_topology.second_countable_topology_of_encodable
{α : Type u_1}
[topological_space α]
[hd : discrete_topology α]
[encodable α] :
@[protected, instance]
def
discrete_topology.order_topology_of_pred_succ'
{α : Type u_1}
[topological_space α]
[h : discrete_topology α]
[partial_order α]
[pred_order α]
[succ_order α]
[no_min_order α]
[no_max_order α] :
@[protected, instance]
def
discrete_topology.order_topology_of_pred_succ
{α : Type u_1}
[topological_space α]
[h : discrete_topology α]
[linear_order α]
[pred_order α]
[succ_order α] :