Documentation

Mathlib.SetTheory.Cardinal.Cofinality.Basic

Cofinality of an order #

This file contains the definition of the cofinality Order.cof α of an order. This is the smallest cardinality of a cofinal subset.

Cofinality of orders #

source
noncomputable def Order.cof (α : Type u) [Preorder α] :
Cardinal.{u}

The cofinality of a preorder is the smallest cardinality of a cofinal subset.

Equations
Instances For
    source
    theorem Order.cof_le {α : Type u} [Preorder α] {s : Set α} (h : IsCofinal s) :
    cof α ≤ Cardinal.mk ↑s
    source
    theorem Order.le_lift_cof_iff {α : Type u} [Preorder α] {c : Cardinal.{max u v}} :
    c ≤ Cardinal.lift.{v, u} (cof α) ↔ ∀ (s : Set α), IsCofinal s → c ≤ Cardinal.lift.{v, u} (Cardinal.mk ↑s)
    source
    theorem Order.le_cof_iff {α : Type u} [Preorder α] {c : Cardinal.{u}} :
    c ≤ cof α ↔ ∀ (s : Set α), IsCofinal s → c ≤ Cardinal.mk ↑s
    source
    theorem Order.exists_cof_eq (α : Type u) [Preorder α] :
    ∃ (s : Set α), IsCofinal s ∧ Cardinal.mk ↑s = cof α

    Every well-order has a cofinal subset of cardinal cof α.

    source
    @[deprecated Order.exists_cof_eq (since := "2026-05-25")]
    theorem Order.cof_eq (α : Type u) [Preorder α] :
    ∃ (s : Set α), IsCofinal s ∧ Cardinal.mk ↑s = cof α

    Alias of Order.exists_cof_eq.

    Every well-order has a cofinal subset of cardinal cof α.

    source
    theorem Order.cof_le_cardinalMk (α : Type u) [Preorder α] :
    cof α ≤ Cardinal.mk α
    source
    theorem Order.cof_eq_zero_iff {α : Type u} [Preorder α] :
    cof α = 0 ↔ IsEmpty α
    source
    @[simp]
    theorem Order.cof_eq_zero {α : Type u} [Preorder α] [h : IsEmpty α] :
    cof α = 0
    source
    theorem Order.cof_ne_zero_iff {α : Type u} [Preorder α] :
    cof α ≠ 0 ↔ Nonempty α
    source
    @[simp]
    theorem Order.cof_ne_zero {α : Type u} [Preorder α] [h : Nonempty α] :
    cof α ≠ 0
    source
    theorem Order.cof_eq_one_iff {α : Type u} [Preorder α] :
    cof α = 1 ↔ ∃ (x : α), IsTop x
    source
    @[simp]
    theorem Order.cof_eq_one {α : Type u} [Preorder α] [OrderTop α] :
    cof α = 1
    source
    theorem Order.cof_ne_one_iff {α : Type u} [Preorder α] :
    cof α ≠ 1 ↔ NoTopOrder α
    source
    @[simp]
    theorem Order.cof_ne_one {α : Type u} [Preorder α] [h : NoTopOrder α] :
    cof α ≠ 1
    source
    theorem Order.cof_le_one_iff {α : Type u} [Preorder α] [Nonempty α] :
    cof α ≤ 1 ↔ ∃ (x : α), IsTop x
    source
    theorem Order.one_lt_cof_iff {α : Type u} [Preorder α] [Nonempty α] :
    1 < cof α ↔ NoTopOrder α
    source
    @[simp]
    theorem Order.one_lt_cof {α : Type u} [Preorder α] [Nonempty α] [h : NoTopOrder α] :
    1 < cof α
    source
    theorem Order.lift_cof_congr_of_strictMono {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : StrictMono f) (hf' : IsCofinal (Set.range f)) :
    Cardinal.lift.{v, u} (cof α) = Cardinal.lift.{u, v} (cof β)
    source
    theorem Order.cof_congr_of_strictMono {α γ : Type u} [LinearOrder α] [LinearOrder γ] {f : α → γ} (hf : StrictMono f) (hf' : IsCofinal (Set.range f)) :
    cof α = cof γ
    source
    theorem Order.cof_eq_of_isCofinal {α : Type u} [LinearOrder α] {s : Set α} (hs : IsCofinal s) :
    cof ↑s = cof α
    source
    @[simp]
    theorem Order.cof_lt_aleph0_iff {α : Type u} [LinearOrder α] :
    cof α < Cardinal.aleph0 ↔ cof α ≤ 1
    source
    @[simp]
    theorem Order.aleph0_le_cof_iff {α : Type u} [LinearOrder α] :
    Cardinal.aleph0 ≤ cof α ↔ 1 < cof α
    source
    theorem Order.aleph0_le_cof {α : Type u} [LinearOrder α] [Nonempty α] [NoMaxOrder α] :
    Cardinal.aleph0 ≤ cof α
    source
    @[simp]
    theorem Order.cof_eq_aleph0 {α : Type u} [LinearOrder α] [NoMaxOrder α] [Nonempty α] [Countable α] :
    cof α = Cardinal.aleph0
    source
    theorem Order.cof_nat :
    cof ℕ = Cardinal.aleph0
    source
    theorem GaloisConnection.cof_le_lift {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : β → α} {g : α → β} (h : GaloisConnection f g) :
    Cardinal.lift.{u, v} (Order.cof β) ≤ Cardinal.lift.{v, u} (Order.cof α)
    source
    theorem GaloisConnection.cof_le {α γ : Type u} [Preorder α] [Preorder γ] {f : γ → α} {g : α → γ} (h : GaloisConnection f g) :
    Order.cof γ ≤ Order.cof α
    source
    theorem OrderIso.lift_cof_congr {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α ≃o β) :
    Cardinal.lift.{v, u} (Order.cof α) = Cardinal.lift.{u, v} (Order.cof β)
    source
    theorem OrderIso.cof_congr {α γ : Type u} [Preorder α] [Preorder γ] (f : α ≃o γ) :
    Order.cof α = Order.cof γ
    source
    theorem isCofinal_of_isCofinal_sUnion {α : Type u_1} [LinearOrder α] {s : Set (Set α)} (h₁ : IsCofinal (⋃₀ s)) (h₂ : Cardinal.mk ↑s < Order.cof α) :
    ∃ x ∈ s, IsCofinal x

    If the union of s is cofinal and s is smaller than the cofinality, then s has a cofinal member.

    source
    theorem isCofinal_of_isCofinal_iUnion {α ι : Type u_1} [LinearOrder α] {s : ι → Set α} (h₁ : IsCofinal (⋃ (i : ι), s i)) (h₂ : Cardinal.mk ι < Order.cof α) :
    ∃ (i : ι), IsCofinal (s i)

    If the union of the ι-indexed family s is cofinal and ι is smaller than the cofinality, then s has a cofinal member.