feat: cofinality within order

Mathlib/SetTheory/Cardinal/Basic.lean

@@ -942,6 +942,14 @@ theorem mk_preimage_of_subset_range (f : α → β) (s : Set β) (h : s ⊆ rang
   rw [← lift_id #(↑(f ⁻¹' s)), ← lift_id #(↑s)]
   exact mk_preimage_of_subset_range_lift f s h
 
+open Set.Notation in
+theorem mk_preimage_val_le_left (s t : Set α) : #(s ↓∩ t) ≤ #s :=
+  mk_set_le _
+
+open Set.Notation in
+theorem mk_preimage_val_le_right (s t : Set α) : #(s ↓∩ t) ≤ #t :=
+  mk_preimage_of_injective _ _ Subtype.val_injective
+
 theorem mk_subset_ge_of_subset_image_lift {α : Type u} {β : Type v} (f : α → β) {s : Set α}
     {t : Set β} (h : t ⊆ f '' s) : lift.{u} #t ≤ lift.{v} #({ x ∈ s | f x ∈ t } : Set α) := by
   rw [image_eq_range] at h

Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean

@@ -17,7 +17,7 @@ cardinality of a cofinal subset.
 
 public noncomputable section
 
-open Function Cardinal Set Order
+open Cardinal Set Order
 
 universe u v w
 
@@ -164,21 +164,21 @@ section Congr
 variable [Preorder α] [Preorder β] [Preorder γ]
 
 theorem GaloisConnection.cof_le_lift {f : β → α} {g : α → β} (h : GaloisConnection f g) :
-    Cardinal.lift.{u} (Order.cof β) ≤ Cardinal.lift.{v} (Order.cof α) := by
+    Cardinal.lift.{u} (cof β) ≤ Cardinal.lift.{v} (cof α) := by
   rw [le_lift_cof_iff]
   exact fun s hs ↦ (lift_le.2 <| cof_le (h.map_isCofinal hs)).trans mk_image_le_lift
 
 theorem GaloisConnection.cof_le {f : γ → α} {g : α → γ} (h : GaloisConnection f g) :
-    Order.cof γ ≤ Order.cof α := by
+    cof γ ≤ cof α := by
   simpa using h.cof_le_lift
 
 theorem OrderIso.lift_cof_congr (f : α ≃o β) :
-    Cardinal.lift.{v} (Order.cof α) = Cardinal.lift.{u} (Order.cof β) :=
+    Cardinal.lift.{v} (cof α) = Cardinal.lift.{u} (cof β) :=
   f.to_galoisConnection.cof_le_lift.antisymm (f.symm.to_galoisConnection.cof_le_lift)
 
 @[deprecated (since := "2026-03-20")] alias OrderIso.lift_cof_eq := OrderIso.lift_cof_congr
 
-theorem OrderIso.cof_congr (f : α ≃o γ) : Order.cof α = Order.cof γ := by
+theorem OrderIso.cof_congr (f : α ≃o γ) : cof α = cof γ := by
   simpa using f.lift_cof_congr
 
 @[deprecated (since := "2026-03-20")] alias OrderIso.cof_eq := OrderIso.cof_congr
@@ -191,7 +191,7 @@ end Congr
 /-- If the union of `s` is cofinal and `s` is smaller than the cofinality, then `s` has a cofinal
 member. -/
 theorem isCofinal_of_isCofinal_sUnion {α : Type*} [LinearOrder α] {s : Set (Set α)}
-    (h₁ : IsCofinal (⋃₀ s)) (h₂ : #s < Order.cof α) : ∃ x ∈ s, IsCofinal x := by
+    (h₁ : IsCofinal (⋃₀ s)) (h₂ : #s < cof α) : ∃ x ∈ s, IsCofinal x := by
   contrapose! h₂
   simp_rw [not_isCofinal_iff] at h₂
   choose f hf using h₂
@@ -202,7 +202,81 @@ theorem isCofinal_of_isCofinal_sUnion {α : Type*} [LinearOrder α] {s : Set (Se
 /-- If the union of the `ι`-indexed family `s` is cofinal and `ι` is smaller than the cofinality,
 then `s` has a cofinal member. -/
 theorem isCofinal_of_isCofinal_iUnion {α : Type*} {ι} [LinearOrder α] {s : ι → Set α}
-    (h₁ : IsCofinal (⋃ i, s i)) (h₂ : #ι < Order.cof α) : ∃ i, IsCofinal (s i) := by
+    (h₁ : IsCofinal (⋃ i, s i)) (h₂ : #ι < cof α) : ∃ i, IsCofinal (s i) := by
   rw [← sUnion_range] at h₁
   obtain ⟨_, ⟨i, rfl⟩, h⟩ := isCofinal_of_isCofinal_sUnion h₁ (mk_range_le.trans_lt h₂)
   exact ⟨i, h⟩
+
+/-! ### Cofinality within order -/
+
+namespace Order
+variable {x : α}
+
+section Preorder
+variable [Preorder α]
+
+/-- The cofinality of an element `x` within a preorder is defined as `cof (Iio x)`. -/
+def cofWithin (x : α) : Cardinal :=
+  cof (Iio x)
+
+@[simp]
+theorem cof_Iio (x : α) : cof (Iio x) = cofWithin x :=
+  (rfl)
+
+theorem cofWithin_le {s : Set α} (hs : IsCofinalFor (Iio x) s) (hsx : s ⊆ Iio x) :
+    cofWithin x ≤ #s := by
+  refine (cof_le fun ⟨y, hy⟩ ↦ ?_).trans <| mk_preimage_val_le_right ..
+  obtain ⟨z, hz, hyz⟩ := hs hy
+  exact ⟨⟨z, hsx hz⟩, hz, hyz⟩
+
+@[simp]
+theorem cofWithin_eq_zero_iff : cofWithin x = 0 ↔ IsMin x := by
+  rw [cofWithin, cof_eq_zero_iff, isEmpty_coe_sort, Iio_eq_empty_iff]
+
+@[simp]
+theorem cofWithin_bot [OrderBot α] : cofWithin (⊥ : α) = 0 :=
+  cofWithin_eq_zero_iff.2 isMin_bot
+
+end Preorder
+
+section LinearOrder
+variable [LinearOrder α] [LinearOrder β]
+
+@[simp]
+theorem cofWithin_lt_aleph0_iff : cofWithin x < ℵ₀ ↔ cofWithin x ≤ 1 :=
+  cof_lt_aleph0_iff
+
+@[simp]
+theorem aleph0_le_cofWithin_iff : ℵ₀ ≤ cofWithin x ↔ 1 < cofWithin x :=
+  aleph0_le_cof_iff
+
+theorem cofWithin_eq_one_iff : cofWithin x = 1 ↔ ¬ IsSuccPrelimit x := by
+  rw [cofWithin, cof_eq_one_iff]
+  unfold IsTop IsSuccPrelimit CovBy
+  simp [← not_lt, imp_not_comm]
+
+theorem cofWithin_ne_one_iff : cofWithin x ≠ 1 ↔ IsSuccPrelimit x := by
+  rw [ne_eq, cofWithin_eq_one_iff, not_not]
+
+theorem cofWithin_le_one_iff : cofWithin x ≤ 1 ↔ ¬ IsSuccLimit x := by
+  rw [Cardinal.le_one_iff, cofWithin_eq_zero_iff, cofWithin_eq_one_iff,
+    IsSuccLimit, not_and_or, not_not]
+
+theorem one_lt_cofWithin_iff : 1 < cofWithin x ↔ IsSuccLimit x := by
+  rw [← not_le, cofWithin_le_one_iff, not_not]
+
+alias ⟨_, IsSuccPrelimit.cofWithin_ne_one⟩ := cofWithin_ne_one_iff
+alias ⟨_, IsSuccLimit.one_lt_cofWithin⟩ := one_lt_cofWithin_iff
+
+theorem IsSuccLimit.cofWithin_ne_one (hx : IsSuccLimit x) : cofWithin x ≠ 1 :=
+  hx.one_lt_cofWithin.ne'
+
+theorem cofWithin_succ_of_not_isMax (hx : ¬ IsMax x) [SuccOrder α] : cofWithin (succ x) = 1 :=
+  cofWithin_eq_one_iff.2 (mt IsSuccPrelimit.isMax hx)
+
+@[simp]
+theorem cofWithin_succ (x : α) [SuccOrder α] [NoMaxOrder α] : cofWithin (succ x) = 1 :=
+  cofWithin_succ_of_not_isMax (not_isMax x)
+
+end LinearOrder
+end Order

Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean

@@ -43,6 +43,7 @@ theorem Order.cof_int : cof ℤ = ℵ₀ := by simp
 namespace Ordinal
 
 /-- The cofinality on an ordinal is the `Order.cof` of any isomorphic linear order.
+This is the same as `Order.cofWithin`, but without the universe bump.
 
 In particular, `cof 0 = 0` and `cof (succ o) = 1`. -/
 def cof (o : Ordinal.{u}) : Cardinal.{u} :=
@@ -61,6 +62,12 @@ theorem cof_type (α : Type*) [LinearOrder α] [WellFoundedLT α] :
 theorem cof_toType (o : Ordinal) : Order.cof o.ToType = o.cof := by
   conv_rhs => rw [← type_toType o, cof_type]
 
+@[simp]
+theorem cof_typein [LinearOrder α] [WellFoundedLT α] (x : α) :
+    cof (typein (α := α) (· < ·) x) = cofWithin x := by
+  rw [← cof_Iio]
+  exact cof_type _
+
 @[deprecated (since := "2026-02-18")] alias cof_eq_cof_toType := cof_toType
 @[deprecated (since := "2026-02-18")] alias le_cof_type := le_cof_iff
 @[deprecated (since := "2026-02-18")] alias cof_type_le := cof_le
@@ -73,13 +80,14 @@ theorem lift_cof (o : Ordinal.{u}) : Cardinal.lift.{v} (cof o) = cof (Ordinal.li
   rw [cof_type, ← type_lt_ulift, cof_type, ← Cardinal.lift_id'.{u, v} (Order.cof (ULift _)),
     ← Cardinal.lift_umax, ← ULift.orderIso.lift_cof_congr]
 
-theorem _root_.Order.cof_Iio [LinearOrder α] [WellFoundedLT α] (x : α) :
-    Order.cof (Iio x) = cof (typein (α := α) (· < ·) x) :=
-  (cof_type _).symm
-
 @[simp]
-theorem cof_Iio (o : Ordinal.{u}) : Order.cof (Iio o) = cof (lift.{u + 1} o) := by
-  rw [Order.cof_Iio, typein_ordinal]
+theorem _root_.Order.cofWithin_ordinal (o : Ordinal.{u}) : cofWithin o = cof (lift.{u + 1} o) := by
+  rw [← cof_typein, typein_ordinal]
+
+@[deprecated cofWithin_ordinal (since := "2026-05-22")]
+protected theorem cof_Iio (o : Ordinal.{u}) : Order.cof (Iio o) = cof (lift.{u + 1} o) := by
+  rw [cof_Iio]
+  exact cofWithin_ordinal o
 
 theorem cof_le_card (o : Ordinal) : cof o ≤ card o := by
   simpa using cof_le_cardinalMk o.ToType
@@ -265,7 +273,7 @@ theorem sSup_add_one_lt_of_lt_cof {s : Set Ordinal.{u}} {a : Ordinal.{u}}
   · simp [hs]
   · rintro rfl
     rw [← lift_cof, ← Cardinal.lift_lt.{_, u + 2}, Cardinal.lift_lift,
-      lift_cof_iSup_add_one fun _ ↦ by simp, cof_Iio, ← lift_cof, cof_type,
+      lift_cof_iSup_add_one fun _ ↦ by simp, cof_Iio, cofWithin_ordinal, ← lift_cof, cof_type,
       Cardinal.lift_lift, Cardinal.lift_lt] at ha
     exact ha.not_ge (cof_le_cardinalMk _)