cof_type_lt

Mathlib/SetTheory/Cardinal/Cofinality.lean

@@ -130,6 +130,13 @@ def cof (o : Ordinal.{u}) : Cardinal.{u} := by
 theorem cof_type (r : α → α → Prop) [IsWellOrder α r] : (type r).cof = Order.cof (swap rᶜ) :=
   rfl
 
+theorem cof_type_lt [LinearOrder α] [IsWellOrder α (· < ·)] :
+    (@type α (· < ·) _).cof = @Order.cof α (· ≤ ·) := by
+  rw [cof_type]
+  congr
+  ext
+  simp [swap]
+
 theorem le_cof_type [IsWellOrder α r] {c} : c ≤ cof (type r) ↔ ∀ S, Unbounded r S → c ≤ #S :=
   (le_csInf_iff'' (Order.cof_nonempty _)).trans
     ⟨fun H S h => H _ ⟨S, h, rfl⟩, by