refactor(order/lattice): generalize directed_of_mono (#1879)

It suffices to have `semilattice_sup`, not `decidable_linear_order`.
Also add `directed_of_antimono`.

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: urkud

src/order/basic.lean

@@ -578,11 +578,6 @@ theorem directed_mono {s : α → α → Prop} {ι} (f : ι → α)
   (H : ∀ a b, r a b → s a b) (h : directed r f) : directed s f :=
 λ a b, let ⟨c, h₁, h₂⟩ := h a b in ⟨c, H _ _ h₁, H _ _ h₂⟩
 
-/-- A monotone function on a linear order is directed. -/
-lemma directed_of_mono {ι} [decidable_linear_order ι] (f : ι → α)
-  (H : ∀ i j, i ≤ j → f i ≼ f j) : directed (≼) f :=
-λ a b, ⟨max a b, H _ _ (le_max_left _ _), H _ _ (le_max_right _ _)⟩
-
 section prio
 set_option default_priority 100 -- see Note [default priority]
 class directed_order (α : Type u) extends preorder α :=

src/order/lattice.lean

@@ -96,6 +96,11 @@ by finish
 theorem le_of_sup_eq (h : a ⊔ b = b) : a ≤ b :=
 by finish
 
+/-- A monotone function on a sup-semilattice is directed. -/
+lemma directed_of_mono {β} (f : α → β) {r : β → β → Prop}
+  (H : ∀ ⦃i j⦄, i ≤ j → r (f i) (f j)) : directed r f :=
+λ a b, ⟨a ⊔ b, H le_sup_left, H le_sup_right⟩
+
 @[simp] lemma sup_lt_iff [is_total α (≤)] {a b c : α} : b ⊔ c < a ↔ b < a ∧ c < a :=
 begin
   cases (is_total.total (≤) b c) with h,
@@ -199,6 +204,11 @@ by finish
 theorem le_of_inf_eq (h : a ⊓ b = a) : a ≤ b :=
 by finish
 
+/-- An antimonotone function on a sup-semilattice is directed. -/
+lemma directed_of_antimono {β} (f : α → β) {r : β → β → Prop}
+  (H : ∀ ⦃i j⦄, i ≤ j → r (f j) (f i)) : directed r f :=
+λ a b, ⟨a ⊓ b, H inf_le_left, H inf_le_right⟩
+
 @[simp] lemma lt_inf_iff [is_total α (≤)] {a b c : α} : a < b ⊓ c ↔ a < b ∧ a < c :=
 begin
   cases (is_total.total (≤) b c) with h,

src/topology/bases.lean

@@ -84,7 +84,7 @@ begin
   refine (has_countable_basis_iff_mono_seq f).trans (exists_congr $ λ x, and_congr_right _),
   intro hmono,
   have : directed (≥) (λ i, principal (x i)),
-    from directed_of_mono _ _ (λ i j hij, principal_mono.2 (hmono _ _ hij)),
+    from directed_of_mono _ (λ i j hij, principal_mono.2 (hmono _ _ hij)),
   simp only [filter.ext_iff, mem_infi this ⟨0⟩, mem_Union, mem_principal_sets]
 end
 

src/topology/sequences.lean

@@ -187,7 +187,7 @@ instance [topological_space α] [first_countable_topology α] : sequential_space
   have gssnhds : ∀ s ∈ 𝓝 p, ∃ i, g i ⊆ s,
   { intro s, rw gbasis, rw mem_infi,
     { simp, intros i hi, use i, assumption },
-    { apply directed_of_mono, intros, apply principal_mono.mpr, apply gmon, assumption },
+    { apply lattice.directed_of_mono, intros, apply principal_mono.mpr, apply gmon, assumption },
     { apply_instance } },
   -- For the sequence (x i) we can now show that a) it lies in M, and b) converges to p.
   ⟨λ i, (x i).val, by intro i; simp [(x i).property.right],