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.

TODO

• Define Order.cof in terms of Cofinal.
• 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.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

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

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

Equations

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

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.map_cofinal {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : β → α} {g : α → β} (h : GaloisConnection f g) {s : Set α} (hs : IsCofinal s) : IsCofinal (g '' s)

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

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_setOf_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.