feat: DirSupClosedOn on linear orders (leanprover-community#38809)

Every subset of a linear order is directed, so we can take off this part of the predicate.

Author: vihdzp

Mathlib/Order/DirSupClosed.lean

@@ -221,6 +221,28 @@ theorem dirSupClosedOn_singleton (a : α) : DirSupClosedOn D {a} :=
 
 end PartialOrder
 
+namespace LinearOrder
+variable [LinearOrder α]
+
+theorem dirSupClosedOn_iff_of_linearOrder :
+    DirSupClosedOn D s ↔ ∀ ⦃d⦄, d ∈ D → d ⊆ s → d.Nonempty → ∀ ⦃a⦄, IsLUB d a → a ∈ s := by
+  simp [DirSupClosedOn]
+
+theorem dirSupClosed_iff_of_linearOrder :
+    DirSupClosed s ↔ ∀ ⦃d⦄, d ⊆ s → d.Nonempty → ∀ ⦃a⦄, IsLUB d a → a ∈ s := by
+  simp [DirSupClosed]
+
+theorem dirSupInaccOn_iff_of_linearOrder :
+    DirSupInaccOn D s ↔
+      ∀ ⦃d⦄, d ∈ D → d.Nonempty → ∀ ⦃a⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty := by
+  simp [DirSupInaccOn]
+
+theorem dirSupInacc_iff_of_linearOrder :
+    DirSupInacc s ↔ ∀ ⦃d⦄, d.Nonempty → ∀ ⦃a⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty := by
+  simp [DirSupInacc]
+
+end LinearOrder
+
 section CompleteLattice
 variable [CompleteLattice α]
 

Mathlib/Order/Directed.lean

@@ -132,6 +132,10 @@ theorem Std.Total.directed [Std.Total r] (f : ι → α) : Directed r f := fun i
 theorem Std.Total.directedOn [Std.Total r] (s : Set α) : DirectedOn r s := fun a ha b hb =>
   Or.casesOn (total_of r a b) (fun h => ⟨b, hb, h, refl _⟩) fun h => ⟨a, ha, refl _, h⟩
 
+@[simp]
+theorem DirectedOn.of_linearOrder [LinearOrder α] (s : Set α) : DirectedOn (· ≤ ·) s :=
+  Std.Total.directedOn s
+
 /-- `IsDirected α r` states that for any elements `a`, `b` there exists an element `c` such that
 `r a c` and `r b c`. -/
 class IsDirected (α : Sort*) (r : α → α → Prop) : Prop where