Documentation

Mathlib.SetTheory.Cardinal.Cofinality

Cofinality #

This file contains the definition of cofinality of an ordinal number and regular cardinals

Main Definitions #

Main Statements #

Implementation Notes #

Tags #

cofinality, regular cardinals, limits cardinals, inaccessible cardinals, infinite pigeonhole principle

Cofinality of orders #

def Order.cof {α : Type u_1} (r : ααProp) :

Cofinality of a reflexive order . This is the smallest cardinality of a subset S : Set α such that ∀ a, ∃ b ∈ S, a ≼ b.

Equations
Instances For
    theorem Order.cof_nonempty {α : Type u_1} (r : ααProp) [IsRefl α r] :
    Set.Nonempty {c : Cardinal.{u_1} | ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) Cardinal.mk S = c}

    The set in the definition of Order.cof is nonempty.

    theorem Order.cof_le {α : Type u_1} (r : ααProp) {S : Set α} (h : ∀ (a : α), ∃ b ∈ S, r a b) :
    theorem Order.le_cof {α : Type u_1} {r : ααProp} [IsRefl α r] (c : Cardinal.{u_1}) :
    c Order.cof r ∀ {S : Set α}, (∀ (a : α), ∃ b ∈ S, r a b)c Cardinal.mk S
    theorem RelIso.cof_le_lift {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [IsRefl β s] (f : r ≃r s) :
    theorem RelIso.cof_eq_lift {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [IsRefl α r] [IsRefl β s] (f : r ≃r s) :
    theorem RelIso.cof_le {α : Type u} {β : Type u} {r : ααProp} {s : ββProp} [IsRefl β s] (f : r ≃r s) :
    theorem RelIso.cof_eq {α : Type u} {β : Type u} {r : ααProp} {s : ββProp} [IsRefl α r] [IsRefl β s] (f : r ≃r s) :
    def StrictOrder.cof {α : Type u_1} (r : ααProp) :

    Cofinality of a strict order . This is the smallest cardinality of a set S : Set α such that ∀ a, ∃ b ∈ S, ¬ b ≺ a.

    Equations
    Instances For
      theorem StrictOrder.cof_nonempty {α : Type u_1} (r : ααProp) [IsIrrefl α r] :
      Set.Nonempty {c : Cardinal.{u_1} | ∃ (S : Set α), Set.Unbounded r S Cardinal.mk S = c}

      The set in the definition of Order.StrictOrder.cof is nonempty.

      Cofinality of ordinals #

      Cofinality of an ordinal. This is the smallest cardinal of a subset S of the ordinal which is unbounded, in the sense ∀ a, ∃ b ∈ S, a ≤ b. It is defined for all ordinals, but cof 0 = 0 and cof (succ o) = 1, so it is only really interesting on limit ordinals (when it is an infinite cardinal).

      Equations
      Instances For
        theorem Ordinal.cof_type {α : Type u_1} (r : ααProp) [IsWellOrder α r] :
        theorem Ordinal.le_cof_type {α : Type u_1} {r : ααProp} [IsWellOrder α r] {c : Cardinal.{u_1}} :
        c Ordinal.cof (Ordinal.type r) ∀ (S : Set α), Set.Unbounded r Sc Cardinal.mk S
        theorem Ordinal.cof_type_le {α : Type u_1} {r : ααProp} [IsWellOrder α r] {S : Set α} (h : Set.Unbounded r S) :
        theorem Ordinal.lt_cof_type {α : Type u_1} {r : ααProp} [IsWellOrder α r] {S : Set α} :
        theorem Ordinal.cof_eq {α : Type u_1} (r : ααProp) [IsWellOrder α r] :
        theorem Ordinal.ord_cof_eq {α : Type u_1} (r : ααProp) [IsWellOrder α r] :

        Cofinality of suprema and least strict upper bounds #

        The set in the lsub characterization of cof is nonempty.

        theorem Ordinal.le_cof_iff_lsub {o : Ordinal.{u}} {a : Cardinal.{u}} :
        a Ordinal.cof o ∀ {ι : Type u} (f : ιOrdinal.{u}), Ordinal.lsub f = oa Cardinal.mk ι
        theorem Ordinal.lsub_lt_ord_lift {ι : Type u} {f : ιOrdinal.{max u v} } {c : Ordinal.{max u v} } (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < Ordinal.cof c) (hf : ∀ (i : ι), f i < c) :
        theorem Ordinal.lsub_lt_ord {ι : Type u} {f : ιOrdinal.{u}} {c : Ordinal.{u}} (hι : Cardinal.mk ι < Ordinal.cof c) :
        (∀ (i : ι), f i < c)Ordinal.lsub f < c
        theorem Ordinal.cof_sup_le {ι : Type u} {f : ιOrdinal.{u}} (H : ∀ (i : ι), f i < Ordinal.sup f) :
        theorem Ordinal.sup_lt_ord_lift {ι : Type u} {f : ιOrdinal.{max u v} } {c : Ordinal.{max u v} } (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < Ordinal.cof c) (hf : ∀ (i : ι), f i < c) :
        theorem Ordinal.sup_lt_ord {ι : Type u} {f : ιOrdinal.{u}} {c : Ordinal.{u}} (hι : Cardinal.mk ι < Ordinal.cof c) :
        (∀ (i : ι), f i < c)Ordinal.sup f < c
        theorem Ordinal.iSup_lt_lift {ι : Type u} {f : ιCardinal.{max u v} } {c : Cardinal.{max u v} } (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < Ordinal.cof (Cardinal.ord c)) (hf : ∀ (i : ι), f i < c) :
        iSup f < c
        theorem Ordinal.iSup_lt {ι : Type u_2} {f : ιCardinal.{u_2}} {c : Cardinal.{u_2}} (hι : Cardinal.mk ι < Ordinal.cof (Cardinal.ord c)) :
        (∀ (i : ι), f i < c)iSup f < c
        theorem Ordinal.nfpFamily_lt_ord_lift {ι : Type u} {f : ιOrdinal.{max u v}Ordinal.{max u v} } {c : Ordinal.{max u v} } (hc : Cardinal.aleph0 < Ordinal.cof c) (hc' : Cardinal.lift.{v, u} (Cardinal.mk ι) < Ordinal.cof c) (hf : ∀ (i : ι), b < c, f i b < c) {a : Ordinal.{max u v} } (ha : a < c) :
        theorem Ordinal.nfpFamily_lt_ord {ι : Type u} {f : ιOrdinal.{u}Ordinal.{u}} {c : Ordinal.{u}} (hc : Cardinal.aleph0 < Ordinal.cof c) (hc' : Cardinal.mk ι < Ordinal.cof c) (hf : ∀ (i : ι), b < c, f i b < c) {a : Ordinal.{u}} :
        a < cOrdinal.nfpFamily f a < c
        theorem Ordinal.nfpBFamily_lt_ord_lift {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v}Ordinal.{max u v} } {c : Ordinal.{max u v} } (hc : Cardinal.aleph0 < Ordinal.cof c) (hc' : Cardinal.lift.{v, u} (Ordinal.card o) < Ordinal.cof c) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), b < c, f i hi b < c) {a : Ordinal.{max u v} } :
        a < cOrdinal.nfpBFamily o f a < c
        theorem Ordinal.nfpBFamily_lt_ord {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{u}Ordinal.{u}} {c : Ordinal.{u}} (hc : Cardinal.aleph0 < Ordinal.cof c) (hc' : Ordinal.card o < Ordinal.cof c) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), b < c, f i hi b < c) {a : Ordinal.{u}} :
        a < cOrdinal.nfpBFamily o f a < c
        theorem Ordinal.nfp_lt_ord {f : Ordinal.{u_2}Ordinal.{u_2}} {c : Ordinal.{u_2}} (hc : Cardinal.aleph0 < Ordinal.cof c) (hf : i < c, f i < c) {a : Ordinal.{u_2}} :
        a < cOrdinal.nfp f a < c
        theorem Ordinal.blsub_lt_ord_lift {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } {c : Ordinal.{max u v} } (ho : Cardinal.lift.{v, u} (Ordinal.card o) < Ordinal.cof c) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) :
        theorem Ordinal.blsub_lt_ord {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{u}} {c : Ordinal.{u}} (ho : Ordinal.card o < Ordinal.cof c) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) :
        theorem Ordinal.cof_bsup_le {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{u}} :
        (∀ (i : Ordinal.{u}) (h : i < o), f i h < Ordinal.bsup o f)Ordinal.cof (Ordinal.bsup o f) Ordinal.card o
        theorem Ordinal.bsup_lt_ord_lift {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{max u v} } {c : Ordinal.{max u v} } (ho : Cardinal.lift.{v, u} (Ordinal.card o) < Ordinal.cof c) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c) :
        theorem Ordinal.bsup_lt_ord {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{u}} {c : Ordinal.{u}} (ho : Ordinal.card o < Ordinal.cof c) :
        (∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c)Ordinal.bsup o f < c

        Basic results #

        @[simp]
        @[simp]

        A fundamental sequence for a is an increasing sequence of length o = cof a that converges at a. We provide o explicitly in order to avoid type rewrites.

        Equations
        Instances For
          theorem Ordinal.IsFundamentalSequence.strict_mono {a : Ordinal.{u}} {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{u}} (hf : Ordinal.IsFundamentalSequence a o f) {i : Ordinal.{u}} {j : Ordinal.{u}} (hi : i < o) (hj : j < o) :
          i < jf i hi < f j hj
          theorem Ordinal.IsFundamentalSequence.monotone {a : Ordinal.{u}} {o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{u}} (hf : Ordinal.IsFundamentalSequence a o f) {i : Ordinal.{u}} {j : Ordinal.{u}} (hi : i < o) (hj : j < o) (hij : i j) :
          f i hi f j hj
          theorem Ordinal.IsFundamentalSequence.trans {a : Ordinal.{u}} {o : Ordinal.{u}} {o' : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < oOrdinal.{u}} (hf : Ordinal.IsFundamentalSequence a o f) {g : (b : Ordinal.{u}) → b < o'Ordinal.{u}} (hg : Ordinal.IsFundamentalSequence o o' g) :
          Ordinal.IsFundamentalSequence a o' fun (i : Ordinal.{u}) (hi : i < o') => f (g i hi)

          Every ordinal has a fundamental sequence.

          theorem Ordinal.IsNormal.isFundamentalSequence {f : Ordinal.{u}Ordinal.{u}} (hf : Ordinal.IsNormal f) {a : Ordinal.{u}} {o : Ordinal.{u}} (ha : Ordinal.IsLimit a) {g : (b : Ordinal.{u}) → b < oOrdinal.{u}} (hg : Ordinal.IsFundamentalSequence a o g) :
          Ordinal.IsFundamentalSequence (f a) o fun (b : Ordinal.{u}) (hb : b < o) => f (g b hb)
          @[simp]
          theorem Ordinal.cof_eq' {α : Type u_1} (r : ααProp) [IsWellOrder α r] (h : Ordinal.IsLimit (Ordinal.type r)) :
          ∃ (S : Set α), (∀ (a : α), ∃ b ∈ S, r a b) Cardinal.mk S = Ordinal.cof (Ordinal.type r)

          Infinite pigeonhole principle #

          theorem Ordinal.unbounded_of_unbounded_sUnion {α : Type u_1} (r : ααProp) [wo : IsWellOrder α r] {s : Set (Set α)} (h₁ : Set.Unbounded r (⋃₀ s)) (h₂ : Cardinal.mk s < StrictOrder.cof r) :
          ∃ x ∈ s, Set.Unbounded r x

          If the union of s is unbounded and s is smaller than the cofinality, then s has an unbounded member

          theorem Ordinal.unbounded_of_unbounded_iUnion {α : Type u} {β : Type u} (r : ααProp) [wo : IsWellOrder α r] (s : βSet α) (h₁ : Set.Unbounded r (⋃ (x : β), s x)) (h₂ : Cardinal.mk β < StrictOrder.cof r) :
          ∃ (x : β), Set.Unbounded r (s x)

          If the union of s is unbounded and s is smaller than the cofinality, then s has an unbounded member

          theorem Ordinal.infinite_pigeonhole {β : Type u} {α : Type u} (f : βα) (h₁ : Cardinal.aleph0 Cardinal.mk β) (h₂ : Cardinal.mk α < Ordinal.cof (Cardinal.ord (Cardinal.mk β))) :
          ∃ (a : α), Cardinal.mk (f ⁻¹' {a}) = Cardinal.mk β

          The infinite pigeonhole principle

          theorem Ordinal.infinite_pigeonhole_card {β : Type u} {α : Type u} (f : βα) (θ : Cardinal.{u}) (hθ : θ Cardinal.mk β) (h₁ : Cardinal.aleph0 θ) (h₂ : Cardinal.mk α < Ordinal.cof (Cardinal.ord θ)) :
          ∃ (a : α), θ Cardinal.mk (f ⁻¹' {a})

          Pigeonhole principle for a cardinality below the cardinality of the domain

          theorem Ordinal.infinite_pigeonhole_set {β : Type u} {α : Type u} {s : Set β} (f : sα) (θ : Cardinal.{u}) (hθ : θ Cardinal.mk s) (h₁ : Cardinal.aleph0 θ) (h₂ : Cardinal.mk α < Ordinal.cof (Cardinal.ord θ)) :
          ∃ (a : α) (t : Set β) (h : t s), θ Cardinal.mk t ∀ ⦃x : β⦄ (hx : x t), f { val := x, property := } = a

          Regular and inaccessible cardinals #

          A cardinal is a strong limit if it is not zero and it is closed under powersets. Note that ℵ₀ is a strong limit by this definition.

          Equations
          Instances For
            theorem Cardinal.mk_bounded_subset {α : Type u_2} (h : x < Cardinal.mk α, 2 ^ x < Cardinal.mk α) {r : ααProp} [IsWellOrder α r] (hr : Cardinal.ord (Cardinal.mk α) = Ordinal.type r) :
            Cardinal.mk { s : Set α // Set.Bounded r s } = Cardinal.mk α

            A cardinal is regular if it is infinite and it equals its own cofinality.

            Equations
            Instances For
              theorem Cardinal.infinite_pigeonhole_card_lt {β : Type u} {α : Type u} (f : βα) (w : Cardinal.mk α < Cardinal.mk β) (w' : Cardinal.aleph0 Cardinal.mk α) :
              ∃ (a : α), Cardinal.mk α < Cardinal.mk (f ⁻¹' {a})

              A function whose codomain's cardinality is infinite but strictly smaller than its domain's has a fiber with cardinality strictly great than the codomain.

              theorem Cardinal.exists_infinite_fiber {β : Type u} {α : Type u} (f : βα) (w : Cardinal.mk α < Cardinal.mk β) (w' : Infinite α) :
              ∃ (a : α), Infinite (f ⁻¹' {a})

              A function whose codomain's cardinality is infinite but strictly smaller than its domain's has an infinite fiber.

              theorem Cardinal.le_range_of_union_finset_eq_top {α : Type u_2} {β : Type u_3} [Infinite β] (f : αFinset β) (w : ⋃ (a : α), (f a) = ) :

              If an infinite type β can be expressed as a union of finite sets, then the cardinality of the collection of those finite sets must be at least the cardinality of β.

              theorem Cardinal.lsub_lt_ord_of_isRegular {ι : Type (max u_2 u_3)} {f : ιOrdinal.{max u_2 u_3} } {c : Cardinal.{max u_2 u_3} } (hc : Cardinal.IsRegular c) (hι : Cardinal.mk ι < c) :
              (∀ (i : ι), f i < Cardinal.ord c)Ordinal.lsub f < Cardinal.ord c
              theorem Cardinal.sup_lt_ord_of_isRegular {ι : Type (max u_2 u_3)} {f : ιOrdinal.{max u_2 u_3} } {c : Cardinal.{max u_2 u_3} } (hc : Cardinal.IsRegular c) (hι : Cardinal.mk ι < c) :
              (∀ (i : ι), f i < Cardinal.ord c)Ordinal.sup f < Cardinal.ord c
              theorem Cardinal.iSup_lt_lift_of_isRegular {ι : Type u} {f : ιCardinal.{max u v} } {c : Cardinal.{max u v} } (hc : Cardinal.IsRegular c) (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < c) :
              (∀ (i : ι), f i < c)iSup f < c
              theorem Cardinal.iSup_lt_of_isRegular {ι : Type u_2} {f : ιCardinal.{u_2}} {c : Cardinal.{u_2}} (hc : Cardinal.IsRegular c) (hι : Cardinal.mk ι < c) :
              (∀ (i : ι), f i < c)iSup f < c
              theorem Cardinal.sum_lt_lift_of_isRegular {ι : Type u} {f : ιCardinal.{max u v} } {c : Cardinal.{max u v} } (hc : Cardinal.IsRegular c) (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < c) (hf : ∀ (i : ι), f i < c) :
              theorem Cardinal.sum_lt_of_isRegular {ι : Type u} {f : ιCardinal.{u}} {c : Cardinal.{u}} (hc : Cardinal.IsRegular c) (hι : Cardinal.mk ι < c) :
              (∀ (i : ι), f i < c)Cardinal.sum f < c
              theorem Cardinal.nfpFamily_lt_ord_of_isRegular {ι : Type u} {f : ιOrdinal.{u}Ordinal.{u}} {c : Cardinal.{u}} (hc : Cardinal.IsRegular c) (hι : Cardinal.mk ι < c) (hc' : c Cardinal.aleph0) {a : Ordinal.{u}} (hf : ∀ (i : ι), b < Cardinal.ord c, f i b < Cardinal.ord c) :
              theorem Cardinal.nfpBFamily_lt_ord_of_isRegular {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{u}Ordinal.{u}} {c : Cardinal.{u}} (hc : Cardinal.IsRegular c) (ho : Ordinal.card o < c) (hc' : c Cardinal.aleph0) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), b < Cardinal.ord c, f i hi b < Cardinal.ord c) {a : Ordinal.{u}} :
              theorem Cardinal.derivFamily_lt_ord {ι : Type u} {f : ιOrdinal.{u}Ordinal.{u}} {c : Cardinal.{u}} (hc : Cardinal.IsRegular c) (hι : Cardinal.mk ι < c) (hc' : c Cardinal.aleph0) (hf : ∀ (i : ι), b < Cardinal.ord c, f i b < Cardinal.ord c) {a : Ordinal.{u}} :
              theorem Cardinal.derivBFamily_lt_ord {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < oOrdinal.{u}Ordinal.{u}} {c : Cardinal.{u}} (hc : Cardinal.IsRegular c) (hι : Ordinal.card o < c) (hc' : c Cardinal.aleph0) (hf : ∀ (i : Ordinal.{u}) (hi : i < o), b < Cardinal.ord c, f i hi b < Cardinal.ord c) {a : Ordinal.{u}} :

              A cardinal is inaccessible if it is an uncountable regular strong limit cardinal.

              Equations
              Instances For
                theorem Cardinal.IsInaccessible.mk {c : Cardinal.{u_2}} (h₁ : Cardinal.aleph0 < c) (h₂ : c Ordinal.cof (Cardinal.ord c)) (h₃ : x < c, 2 ^ x < c) :