Instances related to the discrete topology #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We prove that the discrete topology is
- first-countable,
- second-countable for an encodable type,
- equal to the order topology in linear orders which are also
pred_orderandsucc_order, - metrizable.
When importing this file and data.nat.succ_pred, the instances second_countable_topology ℕ
and order_topology ℕ become available.
@[protected, instance]
@[protected, instance]
def
discrete_topology.second_countable_topology_of_encodable
{α : Type u_1}
[topological_space α]
[hd : discrete_topology α]
[encodable α] :
theorem
bot_topological_space_eq_generate_from_of_pred_succ_order
{α : Type u_1}
[partial_order α]
[pred_order α]
[succ_order α]
[no_min_order α]
[no_max_order α] :
theorem
discrete_topology_iff_order_topology_of_pred_succ'
{α : Type u_1}
[topological_space α]
[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 α]
[partial_order α]
[pred_order α]
[succ_order α]
[no_min_order α]
[no_max_order α] :
theorem
linear_order.bot_topological_space_eq_generate_from
{α : Type u_1}
[linear_order α]
[pred_order α]
[succ_order α] :
theorem
discrete_topology_iff_order_topology_of_pred_succ
{α : Type u_1}
[topological_space α]
[linear_order α]
[pred_order α]
[succ_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 α] :
@[protected, instance]