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