Commit 2026-03-23 09:21 a0d83538
View on Github →feat: cofinalities of suprema (#36924)
We prove that cof (⨆ i : α, f i + 1) = cof α for a strictly monotonic function f. As a corollary, cof (⨆ i : α, f i) = cof α when α has no maximum.
feat: cofinalities of suprema (#36924)
We prove that cof (⨆ i : α, f i + 1) = cof α for a strictly monotonic function f. As a corollary, cof (⨆ i : α, f i) = cof α when α has no maximum.