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