finish

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/Club.lean

@@ -189,11 +189,6 @@ theorem not_isStationary_union [WellFoundedLT α] (hα : cof α ≠ ℵ₀)
   refine ⟨_, hu.inter hα hv, ?_⟩
   grind
 
-theorem dirSupClosed_of_type_le_omega0 [WellFoundedLT α] {s : Set α} (hs : typeLT s ≤ ω) :
-    DirSupClosed s := by
-  
-  sorry
-
 theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal (sᶜ)) : IsStationary s := by
   intro t ht
   obtain ⟨a, ha⟩ := not_isCofinal_iff.1 hs
@@ -205,6 +200,9 @@ theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal (sᶜ)) : IsStati
 theorem isStationary_iff_not_isCofinal_compl [WellFoundedLT α] (hα : cof α ≤ ℵ₀) :
     IsStationary s ↔ ¬ IsCofinal (sᶜ) where
   mp hs h := by
-    obtain ⟨t, ht, ht', htα⟩ := Ordinal.ord_cof_eq_of_isCofinal h
-    sorry
+    obtain ⟨t, hts, ht, htα⟩ := ord_cof_eq_of_isCofinal h
+    have ht' := dirSupClosed_of_type_le_omega0 ht (htα.trans_le ?_)
+    · cases hs ⟨ht', ht⟩
+      grind
+    · simpa using ord_mono hα
   mpr := .of_not_isCofinal_compl

Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean

@@ -195,13 +195,20 @@ 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) (hs' : typeLT s ≤ ω) : DirSupClosed s := by
-  obtain rfl | hs₀ := s.eq_empty_or_nonempty
-  · simp
-  let f (n : ℕ) : α := if hn : n < typeLT s then enum (· < · : s → _) ⟨n, hn⟩
-  sorry
+    {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
 
-#exit
 /-! ### Cofinalities and suprema -/
 
 section LinearOrder