feat(topology/order/basic): replace partial_order by preorder (#18064)

It turns out nearly all `partial_order` hypotheses can be generalized to `preorder` in this file.

Author: alreadydone

src/topology/order/basic.lean

@@ -87,7 +87,7 @@ set of points `(x, y)` with `x ≤ y` is closed in the product space. We introdu
 This property is satisfied for the order topology on a linear order, but it can be satisfied more
 generally, and suffices to derive many interesting properties relating order and topology. -/
 class order_closed_topology (α : Type*) [topological_space α] [preorder α] : Prop :=
-(is_closed_le' : is_closed {p:α×α | p.1 ≤ p.2})
+(is_closed_le' : is_closed {p : α × α | p.1 ≤ p.2})
 
 instance [topological_space α] [h : first_countable_topology α] : first_countable_topology αᵒᵈ := h
 
@@ -718,7 +718,7 @@ it on a preorder, but it is mostly interesting in linear orders, where it is als
 We define it as a mixin. If you want to introduce the order topology on a preorder, use
 `preorder.topology`. -/
 class order_topology (α : Type*) [t : topological_space α] [preorder α] : Prop :=
-(topology_eq_generate_intervals : t = generate_from {s | ∃a, s = Ioi a ∨ s = Iio a})
+(topology_eq_generate_intervals : t = generate_from {s | ∃ a, s = Ioi a ∨ s = Iio a})
 
 /-- (Order) topology on a partial order `α` generated by the subbase of open intervals
 `(a, ∞) = { x ∣ a < x }, (-∞ , b) = {x ∣ x < b}` for all `a, b` in `α`. We do not register it as an
@@ -729,23 +729,23 @@ generate_from {s : set α | ∃ (a : α), s = {b : α | a < b} ∨ s = {b : α |
 
 section order_topology
 
-instance {α : Type*} [topological_space α] [partial_order α] [order_topology α] :
-  order_topology αᵒᵈ :=
-⟨by convert @order_topology.topology_eq_generate_intervals α _ _ _;
-  conv in (_ ∨ _) { rw or.comm }; refl⟩
+section preorder
 
-section partial_order
-variables [topological_space α] [partial_order α] [t : order_topology α]
+variables [topological_space α] [preorder α] [t : order_topology α]
 include t
 
+instance : order_topology αᵒᵈ :=
+⟨by convert @order_topology.topology_eq_generate_intervals α _ _ _;
+  conv in (_ ∨ _) { rw or.comm }; refl⟩
+
 lemma is_open_iff_generate_intervals {s : set α} :
-  is_open s ↔ generate_open {s | ∃a, s = Ioi a ∨ s = Iio a} s :=
+  is_open s ↔ generate_open {s | ∃ a, s = Ioi a ∨ s = Iio a} s :=
 by rw [t.topology_eq_generate_intervals]; refl
 
-lemma is_open_lt' (a : α) : is_open {b:α | a < b} :=
+lemma is_open_lt' (a : α) : is_open {b : α | a < b} :=
 by rw [@is_open_iff_generate_intervals α _ _ t]; exact generate_open.basic _ ⟨a, or.inl rfl⟩
 
-lemma is_open_gt' (a : α) : is_open {b:α | b < a} :=
+lemma is_open_gt' (a : α) : is_open {b : α | b < a} :=
 by rw [@is_open_iff_generate_intervals α _ _ t]; exact generate_open.basic _ ⟨a, or.inr rfl⟩
 
 lemma lt_mem_nhds {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 b, a < x :=
@@ -761,7 +761,7 @@ lemma ge_mem_nhds {a b : α} (h : a < b) : ∀ᶠ x in 𝓝 a, x ≤ b :=
 (𝓝 a).sets_of_superset (gt_mem_nhds h) $ assume b hb, le_of_lt hb
 
 lemma nhds_eq_order (a : α) :
-  𝓝 a = (⨅b ∈ Iio a, 𝓟 (Ioi b)) ⊓ (⨅b ∈ Ioi a, 𝓟 (Iio b)) :=
+  𝓝 a = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ (⨅ b ∈ Ioi a, 𝓟 (Iio b)) :=
 by rw [t.topology_eq_generate_intervals, nhds_generate_from];
 from le_antisymm
   (le_inf
@@ -823,7 +823,7 @@ by rw [nhds_order_unbounded hu hl];
 from (tendsto_infi.2 $ assume l, tendsto_infi.2 $ assume hl,
   tendsto_infi.2 $ assume u, tendsto_infi.2 $ assume hu, tendsto_principal.2 $ h l u hl hu)
 
-end partial_order
+end preorder
 
 instance tendsto_Ixx_nhds_within {α : Type*} [preorder α] [topological_space α]
   (a : α) {s t : set α} {Ixx}
@@ -832,7 +832,7 @@ instance tendsto_Ixx_nhds_within {α : Type*} [preorder α] [topological_space 
 filter.tendsto_Ixx_class_inf
 
 instance tendsto_Icc_class_nhds_pi {ι : Type*} {α : ι → Type*}
-  [Π i, partial_order (α i)] [Π i, topological_space (α i)] [∀ i, order_topology (α i)]
+  [Π i, preorder (α i)] [Π i, topological_space (α i)] [∀ i, order_topology (α i)]
   (f : Π i, α i) :
   tendsto_Ixx_class Icc (𝓝 f) (𝓝 f) :=
 begin
@@ -846,7 +846,7 @@ begin
 end
 
 theorem induced_order_topology' {α : Type u} {β : Type v}
-  [partial_order α] [ta : topological_space β] [partial_order β] [order_topology β]
+  [preorder α] [ta : topological_space β] [preorder β] [order_topology β]
   (f : α → β) (hf : ∀ {x y}, f x < f y ↔ x < y)
   (H₁ : ∀ {a x}, x < f a → ∃ b < a, x ≤ f b)
   (H₂ : ∀ {a x}, f a < x → ∃ b > a, f b ≤ x) :
@@ -875,7 +875,7 @@ begin
 end
 
 theorem induced_order_topology {α : Type u} {β : Type v}
-  [partial_order α] [ta : topological_space β] [partial_order β] [order_topology β]
+  [preorder α] [ta : topological_space β] [preorder β] [order_topology β]
   (f : α → β) (hf : ∀ {x y}, f x < f y ↔ x < y)
   (H : ∀ {x y}, x < y → ∃ a, x < f a ∧ f a < y) :
   @order_topology _ (induced f ta) _ :=
@@ -932,24 +932,24 @@ begin
       exact λ hx, ht.out a.2 y.2 ⟨le_of_lt h, le_of_not_gt hx⟩ } }
 end
 
-lemma nhds_within_Ici_eq'' [topological_space α] [partial_order α] [order_topology α] (a : α) :
+lemma nhds_within_Ici_eq'' [topological_space α] [preorder α] [order_topology α] (a : α) :
   𝓝[≥] a = (⨅ u (hu : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a) :=
 begin
   rw [nhds_within, nhds_eq_order],
   refine le_antisymm (inf_le_inf_right _ inf_le_right) (le_inf (le_inf _ inf_le_left) inf_le_right),
   exact inf_le_right.trans (le_infi₂ $ λ l hl, principal_mono.2 $ Ici_subset_Ioi.2 hl)
 end
 
-lemma nhds_within_Iic_eq'' [topological_space α] [partial_order α] [order_topology α] (a : α) :
+lemma nhds_within_Iic_eq'' [topological_space α] [preorder α] [order_topology α] (a : α) :
   𝓝[≤] a = (⨅ l < a, 𝓟 (Ioi l)) ⊓ 𝓟 (Iic a) :=
 nhds_within_Ici_eq'' (to_dual a)
 
-lemma nhds_within_Ici_eq' [topological_space α] [partial_order α] [order_topology α] {a : α}
+lemma nhds_within_Ici_eq' [topological_space α] [preorder α] [order_topology α] {a : α}
   (ha : ∃ u, a < u) :
   𝓝[≥] a = ⨅ u (hu : a < u), 𝓟 (Ico a u) :=
 by simp only [nhds_within_Ici_eq'', binfi_inf ha, inf_principal, Iio_inter_Ici]
 
-lemma nhds_within_Iic_eq' [topological_space α] [partial_order α] [order_topology α] {a : α}
+lemma nhds_within_Iic_eq' [topological_space α] [preorder α] [order_topology α] {a : α}
   (ha : ∃ l, l < a) :
   𝓝[≤] a = ⨅ l < a, 𝓟 (Ioc l a) :=
 by simp only [nhds_within_Iic_eq'', binfi_inf ha, inf_principal, Ioi_inter_Iic]
@@ -973,11 +973,11 @@ lemma nhds_within_Iic_basis [topological_space α] [linear_order α] [order_topo
   [no_min_order α] (a : α) : (𝓝[≤] a).has_basis (λ l, l < a) (λ l, Ioc l a) :=
 nhds_within_Iic_basis' (exists_lt a)
 
-lemma nhds_top_order [topological_space α] [partial_order α] [order_top α] [order_topology α] :
+lemma nhds_top_order [topological_space α] [preorder α] [order_top α] [order_topology α] :
   𝓝 (⊤:α) = (⨅l (h₂ : l < ⊤), 𝓟 (Ioi l)) :=
 by simp [nhds_eq_order (⊤:α)]
 
-lemma nhds_bot_order [topological_space α] [partial_order α] [order_bot α] [order_topology α] :
+lemma nhds_bot_order [topological_space α] [preorder α] [order_bot α] [order_topology α] :
   𝓝 (⊥:α) = (⨅l (h₂ : ⊥ < l), 𝓟 (Iio l)) :=
 by simp [nhds_eq_order (⊥:α)]
 
@@ -1004,7 +1004,7 @@ lemma nhds_bot_basis_Iic [topological_space α] [linear_order α] [order_bot α]
   (𝓝 ⊥).has_basis (λ a : α, ⊥ < a) Iic :=
 @nhds_top_basis_Ici αᵒᵈ _ _ _ _ _ _
 
-lemma tendsto_nhds_top_mono [topological_space β] [partial_order β] [order_top β] [order_topology β]
+lemma tendsto_nhds_top_mono [topological_space β] [preorder β] [order_top β] [order_topology β]
   {l : filter α} {f g : α → β} (hf : tendsto f l (𝓝 ⊤)) (hg : f ≤ᶠ[l] g) :
   tendsto g l (𝓝 ⊤) :=
 begin
@@ -1013,17 +1013,17 @@ begin
   filter_upwards [hf x hx, hg] with _ using lt_of_lt_of_le,
 end
 
-lemma tendsto_nhds_bot_mono [topological_space β] [partial_order β] [order_bot β] [order_topology β]
+lemma tendsto_nhds_bot_mono [topological_space β] [preorder β] [order_bot β] [order_topology β]
   {l : filter α} {f g : α → β} (hf : tendsto f l (𝓝 ⊥)) (hg : g ≤ᶠ[l] f) :
   tendsto g l (𝓝 ⊥) :=
 @tendsto_nhds_top_mono α βᵒᵈ _ _ _ _ _ _ _ hf hg
 
-lemma tendsto_nhds_top_mono' [topological_space β] [partial_order β] [order_top β]
+lemma tendsto_nhds_top_mono' [topological_space β] [preorder β] [order_top β]
   [order_topology β] {l : filter α} {f g : α → β} (hf : tendsto f l (𝓝 ⊤)) (hg : f ≤ g) :
   tendsto g l (𝓝 ⊤) :=
 tendsto_nhds_top_mono hf (eventually_of_forall hg)
 
-lemma tendsto_nhds_bot_mono' [topological_space β] [partial_order β] [order_bot β]
+lemma tendsto_nhds_bot_mono' [topological_space β] [preorder β] [order_bot β]
   [order_topology β] {l : filter α} {f g : α → β} (hf : tendsto f l (𝓝 ⊥)) (hg : g ≤ f) :
   tendsto g l (𝓝 ⊥) :=
 tendsto_nhds_bot_mono hf (eventually_of_forall hg)