Documentation

Mathlib.SetTheory.ZFC.Rank

Ordinal ranks of PSet and ZFSet #

In this file, we define the ordinal ranks of PSet and ZFSet. These ranks are the same as IsWellFounded.rank over ∈, but are defined in a way that the universe levels of ranks are the same as the indexing types.

Definitions #

PSet rank #

source
noncomputable def PSet.rank :
PSet.{u} → Ordinal.{u}

The ordinal rank of a pre-set

Equations
Instances For
    source
    theorem PSet.rank_congr {x y : PSet.{u_1}} :
    x.Equiv y → x.rank = y.rank
    source
    theorem PSet.rank_lt_of_mem {x y : PSet.{u_1}} :
    y ∈ x → y.rank < x.rank
    source
    theorem PSet.rank_le_iff {o : Ordinal.{u_1}} {x : PSet.{u_1}} :
    x.rank ≤ o ↔ ∀ ⦃y : PSet.{u_1}⦄, y ∈ x → y.rank < o
    source
    theorem PSet.lt_rank_iff {o : Ordinal.{u_1}} {x : PSet.{u_1}} :
    o < x.rank ↔ ∃ y ∈ x, o ≤ y.rank
    source
    theorem PSet.rank_mono {x y : PSet.{u}} (h : x ⊆ y) :
    x.rank ≤ y.rank
    source
    @[simp]
    theorem PSet.rank_empty :
    ∅.rank = 0
    source
    @[simp]
    theorem PSet.rank_insert (x y : PSet.{u_1}) :
    (insert x y).rank = max (Order.succ x.rank) y.rank
    source
    @[simp]
    theorem PSet.rank_singleton (x : PSet.{u_1}) :
    {x}.rank = Order.succ x.rank
    source
    theorem PSet.rank_pair (x y : PSet.{u_1}) :
    {x, y}.rank = max (Order.succ x.rank) (Order.succ y.rank)
    source
    @[simp]
    theorem PSet.rank_powerset (x : PSet.{u_1}) :
    x.powerset.rank = Order.succ x.rank
    source
    theorem PSet.rank_sUnion_le (x : PSet.{u_1}) :
    (⋃₀ x).rank ≤ x.rank

    For the rank of ⋃₀ x, we only have rank (⋃₀ x) ≤ rank x ≤ rank (⋃₀ x) + 1.

    This inequality is split into rank_sUnion_le and le_succ_rank_sUnion.

    source
    theorem PSet.le_succ_rank_sUnion (x : PSet.{u_1}) :
    x.rank ≤ Order.succ (⋃₀ x).rank
    source
    theorem PSet.rank_eq_wfRank {x : PSet.{u}} :
    Ordinal.lift.{u + 1, u} x.rank = IsWellFounded.rank (fun (x1 x2 : PSet.{u}) => x1 ∈ x2) x

    PSet.rank is equal to the IsWellFounded.rank over ∈.

    ZFSet rank #

    source
    noncomputable def ZFSet.rank :
    ZFSet.{u} → Ordinal.{u}

    The ordinal rank of a ZFC set

    Equations
    Instances For
      source
      theorem ZFSet.rank_lt_of_mem {x y : ZFSet.{u}} :
      y ∈ x → y.rank < x.rank
      source
      theorem ZFSet.rank_le_iff {x : ZFSet.{u}} {o : Ordinal.{u}} :
      x.rank ≤ o ↔ ∀ ⦃y : ZFSet.{u}⦄, y ∈ x → y.rank < o
      source
      theorem ZFSet.lt_rank_iff {x : ZFSet.{u}} {o : Ordinal.{u}} :
      o < x.rank ↔ ∃ y ∈ x, o ≤ y.rank
      source
      theorem ZFSet.rank_mono {x y : ZFSet.{u}} (h : x ⊆ y) :
      x.rank ≤ y.rank
      source
      @[simp]
      theorem ZFSet.rank_empty :
      ∅.rank = 0
      source
      @[simp]
      theorem ZFSet.rank_insert (x y : ZFSet.{u_1}) :
      (insert x y).rank = max (Order.succ x.rank) y.rank
      source
      @[simp]
      theorem ZFSet.rank_singleton (x : ZFSet.{u_1}) :
      {x}.rank = Order.succ x.rank
      source
      theorem ZFSet.rank_pair (x y : ZFSet.{u_1}) :
      {x, y}.rank = max (Order.succ x.rank) (Order.succ y.rank)
      source
      @[simp]
      theorem ZFSet.rank_union (x y : ZFSet.{u_1}) :
      (x ∪ y).rank = max x.rank y.rank
      source
      @[simp]
      theorem ZFSet.rank_powerset (x : ZFSet.{u_1}) :
      x.powerset.rank = Order.succ x.rank
      source
      theorem ZFSet.rank_sUnion_le (x : ZFSet.{u_1}) :
      (⋃₀ x).rank ≤ x.rank

      For the rank of ⋃₀ x, we only have rank (⋃₀ x) ≤ rank x ≤ rank (⋃₀ x) + 1.

      This inequality is split into rank_sUnion_le and le_succ_rank_sUnion.

      source
      theorem ZFSet.le_succ_rank_sUnion (x : ZFSet.{u_1}) :
      x.rank ≤ Order.succ (⋃₀ x).rank
      source
      @[simp]
      theorem ZFSet.rank_range {α : Type u_1} [Small.{u, u_1} α] (f : α → ZFSet.{u}) :
      (range f).rank = ⨆ (i : α), Order.succ (f i).rank
      source
      theorem ZFSet.rank_eq_wfRank {x : ZFSet.{u}} :
      Ordinal.lift.{u + 1, u} x.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) => x1 ∈ x2) x

      ZFSet.rank is equal to the IsWellFounded.rank over ∈.