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 #

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

The ordinal rank of a pre-set

Equations
Instances For
    source
    theorem PSet.rank_congr {x y : PSet} :
    x.Equiv y → x.rank = y.rank
    source
    theorem PSet.rank_lt_of_mem {x y : PSet} :
    y ∈ x → y.rank < x.rank
    source
    theorem PSet.rank_le_iff {o : Ordinal.{u_1}} {x : PSet} :
    x.rank ≤ o ↔ ∀ ⦃y : PSet⦄, y ∈ x → y.rank < o
    source
    theorem PSet.lt_rank_iff {o : Ordinal.{u_1}} {x : PSet} :
    o < x.rank ↔ ∃ y ∈ x, o ≤ y.rank
    source
    theorem PSet.rank_mono {x y : PSet} (h : x ⊆ y) :
    x.rank ≤ y.rank
    source
    @[simp]
    theorem PSet.rank_empty :
    ∅.rank = 0
    source
    @[simp]
    theorem PSet.rank_insert {x y : PSet} :
    (insert x y).rank = Order.succ x.rank ⊔ y.rank
    source
    @[simp]
    theorem PSet.rank_singleton {x : PSet} :
    {x}.rank = Order.succ x.rank
    source
    theorem PSet.rank_pair {x y : PSet} :
    {x, y}.rank = Order.succ x.rank ⊔ Order.succ y.rank
    source
    @[simp]
    theorem PSet.rank_powerset {x : PSet} :
    x.powerset.rank = Order.succ x.rank
    source
    theorem PSet.rank_sUnion_le {x : PSet} :
    (⋃₀ 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} :
    x.rank ≤ Order.succ (⋃₀ x).rank
    source
    theorem PSet.rank_eq_wfRank {x : PSet} :
    Ordinal.lift.{u + 1, u} x.rank = IsWellFounded.rank (fun (x1 x2 : PSet) => x1 ∈ x2) x

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

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

    The ordinal rank of a ZFC set

    Equations
    Instances For
      source
      theorem ZFSet.rank_lt_of_mem {x y : ZFSet} :
      y ∈ x → y.rank < x.rank
      source
      theorem ZFSet.rank_le_iff {x : ZFSet} {o : Ordinal.{u}} :
      x.rank ≤ o ↔ ∀ ⦃y : ZFSet⦄, y ∈ x → y.rank < o
      source
      theorem ZFSet.lt_rank_iff {x : ZFSet} {o : Ordinal.{u}} :
      o < x.rank ↔ ∃ y ∈ x, o ≤ y.rank
      source
      theorem ZFSet.rank_mono {x y : ZFSet} (h : x ⊆ y) :
      x.rank ≤ y.rank
      source
      @[simp]
      theorem ZFSet.rank_empty :
      ∅.rank = 0
      source
      @[simp]
      theorem ZFSet.rank_insert {x y : ZFSet} :
      (insert x y).rank = Order.succ x.rank ⊔ y.rank
      source
      @[simp]
      theorem ZFSet.rank_singleton {x : ZFSet} :
      {x}.rank = Order.succ x.rank
      source
      theorem ZFSet.rank_pair {x y : ZFSet} :
      {x, y}.rank = Order.succ x.rank ⊔ Order.succ y.rank
      source
      @[simp]
      theorem ZFSet.rank_union {x y : ZFSet} :
      (x ∪ y).rank = x.rank ⊔ y.rank
      source
      @[simp]
      theorem ZFSet.rank_powerset {x : ZFSet} :
      x.powerset.rank = Order.succ x.rank
      source
      theorem ZFSet.rank_sUnion_le {x : ZFSet} :
      (⋃₀ 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} :
      x.rank ≤ Order.succ (⋃₀ x).rank
      source
      @[simp]
      theorem ZFSet.rank_range {α : Type u} {f : α → ZFSet} :
      (ZFSet.range f).rank = Ordinal.lsub fun (i : α) => (f i).rank
      source
      theorem ZFSet.rank_eq_wfRank {x : ZFSet} :
      Ordinal.lift.{u + 1, u} x.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet) => x1 ∈ x2) x

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