Cofinal sets

A set s in an ordered type α is cofinal when for every a : α there exists an element of s greater or equal to it. This file provides a basic API for the IsCofinal predicate.

For the cofinality of a set as a cardinal, see Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean.

TODO

• Deprecate Order.Cofinal in favor of this predicate.

theorem IsCofinal.of_isEmpty {α : Type u_1} [LE α] [IsEmpty α] {s : Set α} : IsCofinal s

theorem isCofinal_empty_iff {α : Type u_1} [LE α] : IsCofinal ∅ ↔ IsEmpty α

theorem IsCofinal.nonempty {α : Type u_1} [LE α] [Nonempty α] {s : Set α} (hs : IsCofinal s) : s.Nonempty

@[simp]

theorem isCofinal_singleton_iff {α : Type u_1} [LE α] {x : α} : IsCofinal {x} ↔ IsTop x

theorem IsCofinal.singleton_top {α : Type u_1} [LE α] [OrderTop α] : IsCofinal {⊤}

theorem IsCofinal.mono {α : Type u_1} [LE α] {s t : Set α} (h : s ⊆ t) (hs : IsCofinal s) : IsCofinal t

@[simp]

theorem IsCofinal.univ {α : Type u_1} [Preorder α] : IsCofinal Set.univ

@[instance_reducible]

instance instInhabitedSubtypeSetIsCofinal {α : Type u_1} [Preorder α] : Inhabited { s : Set α // IsCofinal s }

Equations

• instInhabitedSubtypeSetIsCofinal = { default := ⟨Set.univ, ⋯⟩ }

theorem IsCofinal.image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} {s : Set α} (hs : IsCofinal s) (hf : Monotone f) (hf' : IsCofinal (Set.range f)) : IsCofinal (f '' s)

theorem IsCofinal.trans {α : Type u_1} [Preorder α] {s : Set α} {t : Set ↑s} (hs : IsCofinal s) (ht : IsCofinal t) : IsCofinal (Subtype.val '' t)

A cofinal subset of a cofinal subset is cofinal.

theorem GaloisConnection.isCofinal_range {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : β → α} {g : α → β} (h : GaloisConnection f g) : IsCofinal (Set.range g)

theorem GaloisConnection.map_isCofinal {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : β → α} {g : α → β} (h : GaloisConnection f g) {s : Set α} (hs : IsCofinal s) : IsCofinal (g '' s)

@[deprecated GaloisConnection.map_isCofinal (since := "2026-03-15")]

theorem GaloisConnection.map_cofinal {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : β → α} {g : α → β} (h : GaloisConnection f g) {s : Set α} (hs : IsCofinal s) : IsCofinal (g '' s)

Alias of GaloisConnection.map_isCofinal.

theorem OrderIso.map_isCofinal {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) {s : Set α} (hs : IsCofinal s) : IsCofinal (⇑e '' s)

@[simp]

theorem OrderIso.map_isCofinal_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) {s : Set α} : IsCofinal (⇑e '' s) ↔ IsCofinal s

@[deprecated OrderIso.map_isCofinal (since := "2026-03-15")]

theorem OrderIso.map_cofinal {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (e : α ≃o β) {s : Set α} (hs : IsCofinal s) : IsCofinal (⇑e '' s)

Alias of OrderIso.map_isCofinal.

theorem isCofinal_iff_iUnion_Iic_eq_univ {α : Type u_1} [Preorder α] {s : Set α} : IsCofinal s ↔ ⋃ i ∈ s, Set.Iic i = Set.univ

theorem isCofinal_iff_iUnion_Iio_eq_univ {α : Type u_1} [Preorder α] [NoMaxOrder α] {s : Set α} : IsCofinal s ↔ ⋃ i ∈ s, Set.Iio i = Set.univ

theorem IsCofinal.mem_of_isMax {α : Type u_1} [PartialOrder α] {s : Set α} {a : α} (ha : IsMax a) (hs : IsCofinal s) : a ∈ s

theorem IsCofinal.top_mem {α : Type u_1} [PartialOrder α] [OrderTop α] {s : Set α} (hs : IsCofinal s) : ⊤ ∈ s

@[simp]

theorem isCofinal_iff_top_mem {α : Type u_1} [PartialOrder α] [OrderTop α] {s : Set α} : IsCofinal s ↔ ⊤ ∈ s

theorem not_isCofinal_iff {α : Type u_1} [LinearOrder α] {s : Set α} : ¬IsCofinal s ↔ ∃ (x : α), ∀ y ∈ s, y < x

theorem BddAbove.of_not_isCofinal {α : Type u_1} [LinearOrder α] {s : Set α} (h : ¬IsCofinal s) : BddAbove s

theorem IsCofinal.of_not_bddAbove {α : Type u_1} [LinearOrder α] {s : Set α} (h : ¬BddAbove s) : IsCofinal s

theorem not_isCofinal_iff_bddAbove {α : Type u_1} [LinearOrder α] [NoMaxOrder α] {s : Set α} : ¬IsCofinal s ↔ BddAbove s

In a linear order with no maximum, cofinal sets are the same as unbounded sets.

theorem not_bddAbove_iff_isCofinal {α : Type u_1} [LinearOrder α] [NoMaxOrder α] {s : Set α} : ¬BddAbove s ↔ IsCofinal s

In a linear order with no maximum, cofinal sets are the same as unbounded sets.

theorem isCofinal_setOfPred_imp_lt {α : Type u_1} [LinearOrder α] (r : α → α → Prop) [h : IsWellFounded α r] : IsCofinal {a : α | ∀ (b : α), r b a → b < a}

The set of "records" (the smallest inputs yielding the highest values) with respect to a well-ordering of α is a cofinal set.

@[deprecated isCofinal_setOfPred_imp_lt (since := "2026-07-09")]

theorem isCofinal_setOf_imp_lt {α : Type u_1} [LinearOrder α] (r : α → α → Prop) [h : IsWellFounded α r] : IsCofinal {a : α | ∀ (b : α), r b a → b < a}

Alias of isCofinal_setOfPred_imp_lt.

---

The set of "records" (the smallest inputs yielding the highest values) with respect to a well-ordering of α is a cofinal set.

theorem isCofinal_range_of_strictMono {α : Type u_1} [LinearOrder α] [WellFoundedLT α] {f : α → α} (hf : StrictMono f) : IsCofinal (Set.range f)