finish

Author: vihdzp

Mathlib/Data/Fintype/Order.lean

@@ -195,6 +195,14 @@ lemma Directed.finite_le {ι κ : Sort*} [Nonempty ι] [Finite κ] {f : ι → 
   simpa using
     (hf.comp_of_surjective PLift.down_surjective).finite_set_le (Set.finite_range (PLift.up ∘ g))
 
+theorem DirectedOn.finite_le {s : Set α} (hs₀ : s.Nonempty) (D : DirectedOn r s)
+    (hs : s.Finite) : ∃ z ∈ s, ∀ i ∈ s, r i z := by
+  have := hs₀.to_subtype
+  have := hs.to_subtype
+  obtain ⟨⟨z, hzs⟩, hz⟩ := D.directed_val.finite_le id
+  use z, hzs
+  simpa using hz
+
 variable [Nonempty α] [Preorder α]
 
 theorem Finite.exists_le [IsDirectedOrder α] (f : β → α) : ∃ M, ∀ i, f i ≤ M :=

Mathlib/Order/DirSupClosed.lean

@@ -5,11 +5,12 @@ Authors: Christopher Hoskin, Violeta Hernández Palacios
 -/
 module
 
+public import Mathlib.Data.Fintype.Order
 public import Mathlib.Order.Antisymmetrization
 public import Mathlib.Order.CompleteLattice.Defs
 public import Mathlib.Order.UpperLower.Basic
 
-import Mathlib.Data.Set.Lattice
+import Mathlib.Data.Nat.Lattice
 
 /-!
 # Sets closed under directed suprema
@@ -300,6 +301,29 @@ theorem dirSupClosed_singleton (a : α) : DirSupClosed {a} := by
 theorem dirSupClosedOn_singleton (a : α) : DirSupClosedOn D {a} :=
   (dirSupClosed_singleton a).dirSupClosedOn
 
+theorem DirSupClosed.of_finite (hs : s.Finite) : DirSupClosed s := by
+  intro t ht ht₀ ht₁ a ha
+  obtain ⟨b, hbt, hb⟩ := ht₁.finite_le ht₀ (hs.subset ht)
+  exact ht <| ha.unique ⟨hb, fun x hx ↦ hx hbt⟩ ▸ hbt
+
+theorem dirSupClosed_range_nat {f : ℕ → α} (hf : Monotone f) (hf' : IsCofinal (.range f)) :
+    DirSupClosed (range f) := by
+  intro s hs hs₀ hs₁ a ha
+  obtain ⟨_, ⟨n, rfl⟩, han⟩ := hf' a
+  obtain rfl | han := han.eq_or_lt
+  · simp
+  have hfb : BddAbove (f ⁻¹' s) := by
+    refine ⟨n, fun m hm ↦ ?_⟩
+    by_contra! hnm
+    exact (ha.1 hm).not_gt (han.trans_le (hf hnm.le))
+  refine ⟨sSup (f ⁻¹' s), IsLUB.unique ⟨?_, ?_⟩ ha⟩ <;> intro x hx
+  · obtain ⟨m, rfl⟩ := hs hx
+    exact hf (le_csSup hfb hx)
+  · apply hx (Nat.sSup_mem _ hfb)
+    obtain ⟨x, hx⟩ := hs₀
+    obtain ⟨m, rfl⟩ := hs hx
+    exact ⟨m, hx⟩
+
 end PartialOrder
 
 section LinearOrder