add result

Author: vihdzp

Mathlib/Order/DirSupClosed.lean

@@ -289,7 +289,7 @@ lemma dirSupInaccOn_Iic (a : α) : DirSupInaccOn D (Iic a) :=
 
 end Preorder
 
-namespace PartialOrder
+section PartialOrder
 variable [PartialOrder α]
 
 theorem dirSupClosed_singleton (a : α) : DirSupClosed {a} := by
@@ -301,7 +301,7 @@ 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
+theorem Set.Finite.dirSupClosed (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

Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean

@@ -151,7 +151,8 @@ theorem cof_omega0 : cof ω = ℵ₀ :=
 
 @[deprecated (since := "2026-02-18")] alias cof_eq_one_iff_is_succ := cof_eq_one_iff
 
-theorem ord_cof_eq (α : Type*) [LinearOrder α] [WellFoundedLT α] :
+variable (α) in
+theorem ord_cof_eq [LinearOrder α] [WellFoundedLT α] :
     ∃ s : Set α, IsCofinal s ∧ typeLT s = (Order.cof α).ord := by
   obtain ⟨s, hs, hs'⟩ := Order.cof_eq α
   obtain ⟨r, hr, hr'⟩ := exists_ord_eq s
@@ -166,8 +167,9 @@ theorem ord_cof_eq (α : Type*) [LinearOrder α] [WellFoundedLT α] :
     · obtain ⟨x, z, hz, rfl⟩ := x
       exact (hz _ hxy').asymm hxy
 
+variable (α) in
 @[simp]
-theorem _root_.Order.cof_ord_cof (α : Type*) [LinearOrder α] [WellFoundedLT α] :
+theorem _root_.Order.cof_ord_cof [LinearOrder α] [WellFoundedLT α] :
     (Order.cof α).ord.cof = Order.cof α := by
   obtain ⟨s, hs, hs'⟩ := ord_cof_eq α
   rw [← hs', cof_type]
@@ -183,6 +185,21 @@ theorem cof_ord_cof (o : Ordinal) : o.cof.ord.cof = o.cof := by
 
 @[deprecated (since := "2026-03-21")] alias cof_cof := cof_ord_cof
 
+theorem dirSupClosed_of_type_le_omega0 [LinearOrder α] [WellFoundedLT α]
+    {s : Set α} (hs : IsCofinal s) (hω : typeLT s ≤ ω) : DirSupClosed s := by
+  obtain hω | hω := hω.lt_or_eq
+  · obtain ⟨n, hn⟩ := lt_omega0.1 hω
+    apply_fun card at hn
+    apply Finite.dirSupClosed
+    rw [Set.Finite, ← mk_lt_aleph0_iff]
+    simp_all
+  · let e : ℕ ≃o s := by
+      rw [omega0, ← lift_id (type _), lift_type_eq] at hω
+      exact OrderIso.ofRelIsoLT hω.some.symm
+    have hfs : .range (Subtype.val ∘ e) = s := by simp
+    rw [← hfs] at hs ⊢
+    exact dirSupClosed_range_nat ((Subtype.mono_coe _).comp e.monotone) hs
+
 /-! ### Cofinalities and suprema -/
 
 section LinearOrder