feat(topology/instances/discrete): instances for the discrete topology (#11349)

Prove `first_countable_topology`, `second_countable_topology` and `order_topology` for the discrete topology under appropriate conditions like `encodable`, or being a linear order with `pred` and `succ`. These instances give in particular `second_countable_topology ℕ` and `order_topology ℕ`



Co-authored-by: RemyDegenne <remydegenne@gmail.com>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>

Author: RemyDegenne

src/order/filter/bases.lean

@@ -862,6 +862,9 @@ end
 @[instance] lemma is_countably_generated_principal (s : set α) : is_countably_generated (𝓟 s) :=
 is_countably_generated_of_seq ⟨λ _, s, infi_const.symm⟩
 
+@[instance] lemma is_countably_generated_pure (a : α) : is_countably_generated (pure a) :=
+by { rw ← principal_singleton, exact is_countably_generated_principal _, }
+
 @[instance] lemma is_countably_generated_bot : is_countably_generated (⊥ : filter α) :=
 @principal_empty α ▸ is_countably_generated_principal _
 

src/order/succ_pred/basic.lean

@@ -111,17 +111,26 @@ protected lemma _root_.has_lt.lt.covby_succ {a b : α} (h : a < b) : a ⋖ succ
 @[simp] lemma covby_succ_of_nonempty_Ioi {a : α} (h : (set.Ioi a).nonempty) : a ⋖ succ a :=
 has_lt.lt.covby_succ h.some_mem
 
+lemma lt_succ_of_not_is_max {a : α} (ha : ¬ is_max a) : a < succ_order.succ a :=
+(le_succ a).lt_of_not_le (λ h, not_exists.2 (maximal_of_succ_le h) (not_is_max_iff.mp ha))
+
+lemma lt_succ_iff_of_not_is_max {a b : α} (ha : ¬ is_max a) : b < succ_order.succ a ↔ b ≤ a :=
+⟨le_of_lt_succ, λ h_le, h_le.trans_lt (lt_succ_of_not_is_max ha)⟩
+
+lemma succ_le_iff_of_not_is_max {a b : α} (ha : ¬ is_max a) : succ a ≤ b ↔ a < b :=
+⟨(lt_succ_of_not_is_max ha).trans_le, succ_le_of_lt⟩
+
 section no_max_order
 variables [no_max_order α] {a b : α}
 
 lemma lt_succ (a : α) : a < succ a :=
-(le_succ a).lt_of_not_le $ λ h, not_exists.2 (maximal_of_succ_le h) (exists_gt a)
+lt_succ_of_not_is_max (not_is_max a)
 
 lemma lt_succ_iff : a < succ b ↔ a ≤ b :=
-⟨le_of_lt_succ, λ h, h.trans_lt $ lt_succ b⟩
+lt_succ_iff_of_not_is_max (not_is_max b)
 
 lemma succ_le_iff : succ a ≤ b ↔ a < b :=
-⟨(lt_succ a).trans_le, succ_le_of_lt⟩
+succ_le_iff_of_not_is_max (not_is_max a)
 
 @[simp] lemma succ_le_succ_iff : succ a ≤ succ b ↔ a ≤ b :=
 ⟨λ h, le_of_lt_succ $ (lt_succ a).trans_le h, λ h, succ_le_of_lt $ h.trans_lt $ lt_succ b⟩
@@ -267,6 +276,28 @@ begin
 end
 
 end complete_lattice
+
+section intervals
+variables [preorder α] [succ_order α]
+
+lemma Iic_eq_Iio_succ' {a : α} (ha : ¬ is_max a) :
+  set.Iic a = set.Iio (succ_order.succ a) :=
+by { ext1 x, rw [set.mem_Iic, set.mem_Iio], exact (lt_succ_iff_of_not_is_max ha).symm, }
+
+lemma Iic_eq_Iio_succ [no_max_order α] (a : α) :
+  set.Iic a = set.Iio (succ_order.succ a) :=
+Iic_eq_Iio_succ' (not_is_max a)
+
+lemma Ioi_eq_Ici_succ' {a : α} (ha : ¬ is_max a) :
+  set.Ioi a = set.Ici (succ_order.succ a) :=
+by { ext1 x, rw [set.mem_Ioi, set.mem_Ici], exact (succ_le_iff_of_not_is_max ha).symm, }
+
+lemma Ioi_eq_Ici_succ [no_max_order α] (a : α) :
+  set.Ioi a = set.Ici (succ_order.succ a) :=
+Ioi_eq_Ici_succ' (not_is_max a)
+
+end intervals
+
 end succ_order
 
 /-! ### Predecessor order -/
@@ -323,17 +354,26 @@ protected lemma _root_.has_lt.lt.pred_covby {a b : α} (h : b < a) : pred a ⋖
 @[simp] lemma pred_covby_of_nonempty_Iio {a : α} (h : (set.Iio a).nonempty) : pred a ⋖ a :=
 has_lt.lt.pred_covby h.some_mem
 
+lemma pred_lt_of_not_is_min {a : α} (ha : ¬ is_min a) : pred_order.pred a < a :=
+(pred_le a).lt_of_not_le (λ h, not_exists.2 (minimal_of_le_pred h) (not_is_min_iff.mp ha))
+
+lemma pred_lt_iff_of_not_is_min {a b : α} (ha : ¬ is_min a) : pred_order.pred a < b ↔ a ≤ b :=
+⟨le_of_pred_lt, λ h_le, (pred_lt_of_not_is_min ha).trans_le h_le⟩
+
+lemma le_pred_iff_of_not_is_min {a b : α} (hb : ¬ is_min b) : a ≤ pred b ↔ a < b :=
+⟨λ h, h.trans_lt (pred_lt_of_not_is_min hb), le_pred_of_lt⟩
+
 section no_min_order
 variables [no_min_order α] {a b : α}
 
 lemma pred_lt (a : α) : pred a < a :=
-(pred_le a).lt_of_not_le $ λ h, not_exists.2 (minimal_of_le_pred h) (exists_lt a)
+pred_lt_of_not_is_min (not_is_min a)
 
 lemma pred_lt_iff : pred a < b ↔ a ≤ b :=
-⟨le_of_pred_lt, (pred_lt a).trans_le⟩
+pred_lt_iff_of_not_is_min (not_is_min a)
 
 lemma le_pred_iff : a ≤ pred b ↔ a < b :=
-⟨λ h, h.trans_lt (pred_lt b), le_pred_of_lt⟩
+le_pred_iff_of_not_is_min (not_is_min b)
 
 @[simp] lemma pred_le_pred_iff : pred a ≤ pred b ↔ a ≤ b :=
 ⟨λ h, le_of_pred_lt $ h.trans_lt (pred_lt b), λ h, le_pred_of_lt $ (pred_lt a).trans_le h⟩
@@ -477,6 +517,28 @@ begin
 end
 
 end complete_lattice
+
+section intervals
+variables [preorder α] [pred_order α]
+
+lemma Ici_eq_Ioi_pred' {a : α} (ha : ¬ is_min a) :
+  set.Ici a = set.Ioi (pred_order.pred a) :=
+by { ext1 x, rw [set.mem_Ici, set.mem_Ioi], exact (pred_lt_iff_of_not_is_min ha).symm, }
+
+lemma Ici_eq_Ioi_pred [no_min_order α] (a : α) :
+  set.Ici a = set.Ioi (pred_order.pred a) :=
+Ici_eq_Ioi_pred' (not_is_min a)
+
+lemma Iio_eq_Iic_pred' {a : α} (ha : ¬ is_min a) :
+  set.Iio a = set.Iic (pred_order.pred a) :=
+by { ext1 x, rw [set.mem_Iio, set.mem_Iic], exact (le_pred_iff_of_not_is_min ha).symm, }
+
+lemma Iio_eq_Iic_pred [no_min_order α] (a : α) :
+  set.Iio a = set.Iic (pred_order.pred a) :=
+Iio_eq_Iic_pred' (not_is_min a)
+
+end intervals
+
 end pred_order
 
 open succ_order pred_order

src/topology/bases.lean

@@ -285,6 +285,10 @@ def dense_seq [separable_space α] [nonempty α] : ℕ → α := classical.some
 
 variable {α}
 
+@[priority 100]
+instance encodable.separable_space [encodable α] : separable_space α :=
+{ exists_countable_dense := ⟨set.univ, set.countable_encodable set.univ, dense_univ⟩ }
+
 /-- In a separable space, a family of nonempty disjoint open sets is countable. -/
 lemma _root_.set.pairwise_disjoint.countable_of_is_open [separable_space α] {ι : Type*}
   {s : ι → set α} {a : set ι} (h : a.pairwise_disjoint s) (ha : ∀ i ∈ a, is_open (s i))

src/topology/instances/discrete.lean

@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2022 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+
+import order.succ_pred.basic
+import topology.algebra.order.basic
+
+/-!
+# 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.basic`, the instances `second_countable_topology ℕ`
+and `order_topology ℕ` become available.
+
+-/
+
+open topological_space set
+
+variables {α : Type*} [topological_space α]
+
+@[priority 100]
+instance discrete_topology.first_countable_topology [discrete_topology α] :
+  first_countable_topology α :=
+{ nhds_generated_countable :=
+    by { rw nhds_discrete, exact filter.is_countably_generated_pure } }
+
+@[priority 100]
+instance discrete_topology.second_countable_topology_of_encodable
+  [hd : discrete_topology α] [encodable α] :
+  second_countable_topology α :=
+begin
+  haveI : ∀ (i : α), second_countable_topology ↥({i} : set α),
+    from λ i, { is_open_generated_countable :=
+      ⟨{univ}, countable_singleton _, by simp only [eq_iff_true_of_subsingleton]⟩, },
+  exact second_countable_topology_of_countable_cover (singletons_open_iff_discrete.mpr hd)
+    (Union_of_singleton α),
+end
+
+@[priority 100]
+instance discrete_topology.order_topology_of_pred_succ' [h : discrete_topology α] [partial_order α]
+  [pred_order α] [succ_order α] [no_min_order α] [no_max_order α] :
+  order_topology α :=
+⟨begin
+  rw h.eq_bot,
+  refine (eq_bot_of_singletons_open (λ a, _)).symm,
+  have h_singleton_eq_inter : {a} = Iio (succ_order.succ a) ∩ Ioi (pred_order.pred a),
+  { suffices h_singleton_eq_inter' : {a} = Iic a ∩ Ici a,
+      by rw [h_singleton_eq_inter', pred_order.Ici_eq_Ioi_pred, succ_order.Iic_eq_Iio_succ],
+    rw [inter_comm, Ici_inter_Iic, Icc_self a], },
+  rw h_singleton_eq_inter,
+  apply is_open.inter,
+  { exact is_open_generate_from_of_mem ⟨succ_order.succ a, or.inr rfl⟩, },
+  { exact is_open_generate_from_of_mem ⟨pred_order.pred a, or.inl rfl⟩, },
+end⟩
+
+@[priority 100]
+instance discrete_topology.order_topology_of_pred_succ [h : discrete_topology α] [linear_order α]
+  [pred_order α] [succ_order α] :
+  order_topology α :=
+⟨begin
+  rw h.eq_bot,
+  refine (eq_bot_of_singletons_open (λ a, _)).symm,
+  have h_singleton_eq_inter : {a} = Iic a ∩ Ici a,
+    by rw [inter_comm, Ici_inter_Iic, Icc_self a],
+  by_cases ha_top : is_top a,
+  { rw [ha_top.Iic_eq, inter_comm, inter_univ] at h_singleton_eq_inter,
+    by_cases ha_bot : is_bot a,
+    { rw ha_bot.Ici_eq at h_singleton_eq_inter,
+      rw h_singleton_eq_inter,
+      apply is_open_univ, },
+    { rw is_bot_iff_is_min at ha_bot,
+      rw pred_order.Ici_eq_Ioi_pred' ha_bot at h_singleton_eq_inter,
+      rw h_singleton_eq_inter,
+      exact is_open_generate_from_of_mem ⟨pred_order.pred a, or.inl rfl⟩, }, },
+  { rw is_top_iff_is_max at ha_top,
+    rw succ_order.Iic_eq_Iio_succ' ha_top at h_singleton_eq_inter,
+    by_cases ha_bot : is_bot a,
+    { rw [ha_bot.Ici_eq, inter_univ] at h_singleton_eq_inter,
+      rw h_singleton_eq_inter,
+      exact is_open_generate_from_of_mem ⟨succ_order.succ a, or.inr rfl⟩, },
+    { rw is_bot_iff_is_min at ha_bot,
+      rw pred_order.Ici_eq_Ioi_pred' ha_bot at h_singleton_eq_inter,
+      rw h_singleton_eq_inter,
+      apply is_open.inter,
+      { exact is_open_generate_from_of_mem ⟨succ_order.succ a, or.inr rfl⟩ },
+      { exact is_open_generate_from_of_mem ⟨pred_order.pred a, or.inl rfl⟩ } } }
+end⟩

src/topology/order.lean

@@ -63,6 +63,10 @@ def generate_from (g : set (set α)) : topological_space α :=
   is_open_inter  := generate_open.inter,
   is_open_sUnion := generate_open.sUnion }
 
+lemma is_open_generate_from_of_mem {g : set (set α)} {s : set α} (hs : s ∈ g) :
+  @is_open _ (generate_from g) s :=
+generate_open.basic s hs
+
 lemma nhds_generate_from {g : set (set α)} {a : α} :
   @nhds α (generate_from g) a = (⨅s∈{s | a ∈ s ∧ s ∈ g}, 𝓟 s) :=
 by rw nhds_def; exact le_antisymm