Clubs and stationary sets

Stream: mathlib4

[Nir Paz]

I'm going to be fomalizing some type-theory set-thery in lean for a university project, starting with theorems about clubs and stationary sets. I'd love some feedback about the definitions/naming before I start proving things.

import Mathlib

open Ordinal

-- using ≤ instead of < for the successor case
def Ordinal.IsUnbounded (S : Set Ordinal) (o : Ordinal) : Prop :=
  (∀ s ∈ S, s < o) ∧ (∀ p < o, ∃ s ∈ S, p ≤ s)

def Ordinal.IsLimitPoint (o : Ordinal) (S : Set Ordinal) : Prop :=
  ∀ p < o, ∃ s ∈ S, p < s

def Ordinal.IsClosed (S : Set Ordinal) (o : Ordinal) : Prop :=
  (∀ s ∈ S, s < o) ∧ (∀ p < o, IsLimitPoint p S → p ∈ S)

def Ordinal.IsClub (S : Set Ordinal) (o : Ordinal) : Prop :=
  IsUnbounded S o ∧ IsClosed S o

def Ordinal.IsStationary (S : Set Ordinal) (o : Ordinal) : Prop :=
  ∀ C, IsClub C o → S ∩ C ≠ ∅

Also, I couldn't find the set of elements in a linear order less then a given element, which might simplify some of the definitions if it exists in mathlib.

[Yaël Dillies]

Nir Paz said:

the set of elements in a linear order less then a given element

This is docs#Set.Iio

[Yaël Dillies]

Isn't Ordinal.IsClosed just IsClosed under the order topology?

[Yaël Dillies]

Also Ordinal.IsLimitPoint doesn't seem mathematically correct. Is o really supposed to be a limit point of any set containing o?

[Yaël Dillies]

S ∩ C ≠ ∅ should be replaced by (S ∩ C).Nonempty

[Nir Paz]

@Yaël Dillies Oh IsLimitPoint is totally wrong, I forget to add s<o

[Nir Paz]

As it is it's any point in the downwards closure

[Nir Paz]

Is using the order topology really better? If I defined it that way I would just prove this equivalent and almost exclusively use it instead

[Nir Paz]

I guess it's a bit cleaner but I wouldn't say it's more obviously the mathematically 'correct' definition

[Yaël Dillies]

The point of using docs#IsClosed is that you don't need to reprove everything yourself, like the complement of closed is open, intersection of closeds is closed, etc...

[Nir Paz]

The approaches I know for these things don't really use anything topological past intersection of closed sets is closed (for example open sets in this topology aren't usefull in any way I know of), so I don't think it's worth it for the few simple lemmas I would have to prove about clubs

[Yaël Dillies]

I mean it's not a huge hassle at all. All you have to do is give Ordinal its order topology and prove the one lemma that says IsClosed s ↔ (∀ s ∈ S, s < o) ∧ (∀ p < o, IsLimitPoint p S → p ∈ S)

[Junyan Xu]

There's some code here (in Lean 3, not using topology).

[Nir Paz]

Thanks, I didn't know this was done before!

[Nir Paz]

I also just noticed that 0 is always a limit point in my code, which might also be a problem in the code you sent? Since the supremum of empty is 0

[Junyan Xu]

Yeah Zulip search isn't ideal and searching for "club" is very slow; I had to add my ID to the search.

In mathlib Order.IsSuccLimit includes 0 (⊥) while Ordinal.IsLimit is not. I guess it depends on your application.

[Nir Paz]

I meant a limit point as in my code, not a limit ordinal (I'll change it to accumulation point, it really is a bad name). I'm saying in the code you sent 0 must be in a club, as it's the supremum of the empty set, and it made me notice the same problem in my code.

[Junyan Xu]

I see, probably we want to assume only the suprema of bounded nonempty sets are in the club.

[Nir Paz]

I finished the proof that the intersection of < o.cof clubs in o is a club in o!

It needs lots of cleaning up before it's mathlib-ready, and I defined a bounded recursion construction on ordinals, boundedLimitRec, which I guess I should generalize with a motive like Π o < l, Sort* instead of a constant type as well.

import Mathlib

noncomputable section

open Classical Cardinal Ordinal Set

universe u

namespace Ordinal

def IsUnbounded (S : Set Ordinal) (o : Ordinal) : Prop :=
  S ⊆ (Iio o) ∧ (∀ p < o, ∃ s ∈ S, p < s)

def IsAcc (o : Ordinal) (S : Set Ordinal) : Prop :=
  0 < o ∧ (∀ p < o, ∃ s ∈ S, s < o ∧ p < s)

def IsClosed (S : Set Ordinal) (o : Ordinal) : Prop :=
  S ⊆ (Iio o) ∧ (∀ p < o, IsAcc p S → p ∈ S)

def IsClub (S : Set Ordinal) (o : Ordinal) : Prop :=
  IsClosed S o ∧ IsUnbounded S o

def IsStationary (S : Set Ordinal) (o : Ordinal) : Prop :=
  ∀ C, IsClub C o → (S ∩ C).Nonempty

open Order

def boundedLimitRec {α : Sort*} (l : Ordinal) (H₁ : α) (H₂ : ∀ o, o < l → α → α)
    (H₃ : ∀ o, o < l → IsLimit o → (∀ o' < o, α) → α) (o : Ordinal) (_ : o < l) : α :=
  limitRecOn (C := fun _ ↦ α) o
  H₁ (fun o ih ↦ (if h : o < l then H₂ o h ih else H₁))
  (fun o ho ih ↦ (if h : o < l then H₃ o h ho ih else H₁))

@[simp]
theorem boundedLimitRec_zero {α} (l H₁ H₂ H₃ h) :
    @boundedLimitRec α l H₁ H₂ H₃ 0 h = H₁ := by
  simp_all only [boundedLimitRec, limitRecOn_zero]

@[simp]
theorem boundedLimitRec_succ {α} (l o H₁ H₂ H₃ ho) :
    @boundedLimitRec α l H₁ H₂ H₃ (succ o) ho = H₂ o (lt_of_le_of_lt (le_succ o) ho)
    (@boundedLimitRec α l H₁ H₂ H₃ o (lt_of_le_of_lt (le_succ o) ho)) := by
  simp only [boundedLimitRec, limitRecOn_succ, lt_of_le_of_lt (le_succ o) ho, reduceDite]

@[simp]
theorem boundedLimitRec_limit {α} (l o H₁ H₂ H₃ h ho) :
    @boundedLimitRec α l H₁ H₂ H₃ o h = H₃ o h ho fun x hx ↦
    @boundedLimitRec α l H₁ H₂ H₃ x (hx.trans h) := by
  simp_all only [boundedLimitRec, limitRecOn_limit, reduceDite]

variable {o : Ordinal.{u}} {S : Set (Set Ordinal)}

theorem isAcc_of_subset {S T : Set Ordinal} (h : S ⊆ T) (ho : Ordinal.IsAcc o S) :
    Ordinal.IsAcc o T :=
  ⟨ho.1, fun p plto ↦ (ho.2 p plto).casesOn fun s hs ↦ ⟨s, h hs.1, hs.2⟩⟩

theorem isClosed_sInter_of_closed (hS : S.Nonempty) (h : ∀ C ∈ S, IsClosed C o) :
    IsClosed (⋂₀ S) o :=
  ⟨fun s hs ↦ by
    rcases hS with ⟨C, CmemS⟩
    exact (h C CmemS).1 ((sInter_subset_of_mem CmemS) hs),
  fun p plto pAcc ↦ by
    rw [mem_sInter]
    intro C CmemS
    exact (h C CmemS).2 p plto (isAcc_of_subset (sInter_subset_of_mem CmemS) pAcc)⟩

theorem isLimit_of_not_succ_of_ne_zero {o : Ordinal} (h : ¬∃ a, o = Order.succ a) (h' : o ≠ 0) :
    IsLimit o := by
  have := zero_or_succ_or_limit o
  simp_all only [not_exists, ne_eq, exists_const, false_or]

theorem inter_suffix_of_isUnbounded {U} (hU : IsUnbounded U o) {p : Ordinal} (hp : p < o) :
    (U ∩ (Ioo p o)).Nonempty := by
  rcases hU.2 p hp with ⟨x, xmemU, pltx⟩
  use x; use xmemU
  use pltx
  exact hU.1 xmemU

/--
Given less than `o.cof` unbounded sets in `o` and some `q < o`, there is a `q < p < o`
such that `Ioo q p` contains an element of every unbounded set.
-/
theorem exists_above_of_lt_cof {p : Ordinal} (hp : p < o) (hSemp : Nonempty S)
    (hSunb : ∀ U ∈ S, IsUnbounded U o) (hScard : #S < Cardinal.lift.{u + 1, u} o.cof) :
    ∃ q, q < o ∧ p < q ∧ (∀ U ∈ S, (U ∩ Ioo p q).Nonempty) := by
  rw [lift_cof] at hScard
  have aux : 0 < #S := pos_iff_ne_zero.mpr fun h ↦ by
    have := (mk_emptyCollection_iff.mp h)
    simp_all only [nonempty_subtype, mem_empty_iff_false, exists_const]
  have : 1 ≤ #S := Cardinal.one_le_iff_pos.mpr aux
  have := (lt_of_le_of_lt this hScard).ne

  have oLim : IsLimit o := by
    have neSucc := mt (@cof_eq_one_iff_is_succ (lift.{u + 1, u} o)).mpr this.symm
    have : lift.{u + 1, u} o ≠ 0 := by
      have : o ≠ 0 := (lt_of_le_of_lt (Ordinal.zero_le p) hp).ne.symm
      exact fun h ↦ by
        have : (0 : Ordinal.{u + 1}) = lift.{u + 1, u} (0 : Ordinal.{u}) := lift_zero.symm
        rw [this] at h
        have := lift_inj.mp h
        trivial
    exact (lift_isLimit o).mp <| isLimit_of_not_succ_of_ne_zero neSucc this

  let f : ↑S → Ordinal := fun U ↦ lift.{u + 1, u} (sInf (U ∩ (Ioo p o)))
  have infMem : ∀ U : S, sInf (↑U ∩ Ioo p o) ∈ ↑U ∩ Ioo p o := fun U ↦
    csInf_mem (inter_suffix_of_isUnbounded (hSunb U.1 U.2) hp : (↑U ∩ Ioo p o).Nonempty)
  have flto : ∀ U : S, f U < lift.{u + 1, u} o := fun U ↦ by
    simp_all only [mem_inter_iff, mem_Ioo, lift_lt, f]
  set q := (Ordinal.sup.{u + 1, u} f) + 1 with qdef
  have qlto : q < lift.{u + 1, u} o := by
    have : sup f < lift.{u + 1, u} o := sup_lt_ord hScard flto
    rw [qdef]
    have := ((lift_isLimit.{u + 1, u} o).mpr oLim).2 (sup.{u + 1, u} f) this
    exact this
  rcases lift_down qlto.le with ⟨q', hq'⟩
  use q'
  have fltq : ∀ U, f U < q := fun U ↦
    lt_of_le_of_lt (le_sup.{u + 1, u} f U) (qdef ▸ lt_add_one (sup f))
  constructor <;> try constructor
  · use lift_lt.mp (hq' ▸ qlto)
  · rcases hSemp with ⟨U, hU⟩
    have pltf : lift.{u + 1, u} p < f ⟨U, hU⟩ := lift_lt.mpr (mem_of_mem_inter_right (infMem ⟨U, hU⟩)).1
    have := lt_of_lt_of_le pltf (fltq ⟨U, hU⟩).le
    rwa [← hq', lift_lt] at this
  intro U hU
  specialize infMem ⟨U, hU⟩; change sInf (U ∩ Ioo p o) ∈ U ∩ Ioo p o at infMem
  specialize fltq ⟨U, hU⟩
  have : f ⟨U, hU⟩ ∈ Ioo (lift.{u + 1, u} p) q := by
    have := lift_lt.{u + 1, u}.mpr infMem.2.1
    use this
  rw [← hq'] at fltq
  rcases lift_down fltq.le with ⟨fUdown, fUlift⟩
  use fUdown
  constructor
  · simp_all only [lift_inj, mem_inter_iff, f]
  · constructor
    exact lift_lt.mp <| fUlift ▸ (this.1)
    exact lift_lt.mp <| hq' ▸ (fUlift ▸ this).2

/--
Given a limit ordinal `o` and a property on pairs of ordinals `P`, such that
for any `p < o` there is a `q < o` above `p` so that `P p q`, we can construct
an increasing `ω`-sequence below `o` that satisfies `P` between every 2 consecutive elements.
Additionaly, the sequence can begin arbitrarily high in `o`. That is, above any `q < o`.
-/
theorem exists_seq_succ_prop (oLim : IsLimit o) {P : Ordinal → Ordinal → Prop}
    (hP : ∀ p < o, ∃ q < o, (p < q ∧ P p q)) {q} (qlto : q < o) : ∃ f : Π p < ω, (Iio o),
    (∀ i : Ordinal.{u}, (hi : i < ω) → P (f i hi) (f (i + 1) (omega_isLimit.2 i hi)))
    ∧ (∀ i : Ordinal.{u}, (hi : i < ω) → (f i hi) < f (i + 1) (omega_isLimit.2 i hi))
    ∧ q < f 0 omega_pos := by
  let H₂ : (p : Ordinal) → p < ω → (Iio o) → (Iio o) := fun p _ fp ↦ by
    let C := choose (hP fp fp.2)
    have hC := (choose_spec (hP fp fp.2)).1
    exact ⟨C, hC⟩
  let H₃ : (w : Ordinal) → w < ω → w.IsLimit → ((o' : Ordinal.{u}) → o' < w → (Iio o)) → (Iio o)
      := fun w _ _ _ ↦ ⟨0, oLim.pos⟩
  let f : Π p < ω, Iio o := @boundedLimitRec (Iio o) ω ⟨q + 1, oLim.succ_lt qlto⟩ H₂ H₃
  use f
  constructor <;> try constructor
  intro n hn
  · simp [f]
    generalize_proofs _ pf
    exact (choose_spec pf).2.2
  · intro i hi
    simp [f, H₂]
    generalize_proofs _ _ _ pf
    exact (choose_spec pf).casesOn fun _ x ↦ x.casesOn fun x _ ↦ x
  simp [f]

/--
If between every 2 consecutive elements of an increasing `δ`-sequence there is an element of `C`,
and `δ` is a limit ordinal, then the supremum of the sequence is an accumulation point of `C`.
-/
theorem isAcc_bsup_of_between {δ : Ordinal} (C : Set Ordinal) (δLim : δ.IsLimit)
    (s : Π o < δ, Ordinal) (sInc : ∀ o, (h : o < δ) → s o h < s (o + 1) (δLim.succ_lt h))
    (h : ∀ o, (h : o < δ) → (C ∩ Ioo (s o h) (s (o + 1) (δLim.succ_lt h))).Nonempty) :
    IsAcc (bsup δ s) C := by
  use (by
    apply (lt_bsup s).mpr
    use 1; use (by exact_mod_cast δLim.nat_lt 1)
    have := (sInc 0 δLim.pos)
    simp_rw [zero_add] at this
    refine' lt_of_le_of_lt (Ordinal.zero_le _) (this))
  intro p pltsup
  rw [lt_bsup] at pltsup
  rcases pltsup with ⟨i, hi, plt⟩
  rcases h i hi with ⟨q, qmemC, qmemIoo⟩
  use q; use qmemC
  constructor
  · exact lt_of_lt_of_le qmemIoo.2 (le_bsup _ _ _)
  · exact plt.trans qmemIoo.1

/--
The intersection of less than `o.cof` clubs in `o` is a club in `o`.
-/
theorem isClub_sInter (hCof : ℵ₀ < o.cof) (hS : ∀ C ∈ S, IsClub C o) (hSemp : S.Nonempty)
    (Scard : #S < Cardinal.lift.{u + 1, u} o.cof) : IsClub (⋂₀ S) o := by
  use isClosed_sInter_of_closed hSemp (fun C CmemS ↦ (hS C CmemS).1)
  use fun x xmem ↦ hSemp.casesOn fun C CmemS ↦ (hS C CmemS).1.1 (xmem C CmemS)
  intro q qlto
  have oLim : IsLimit o := aleph0_le_cof.mp hCof.le
  have nonemptyS : Nonempty S := Nonempty.to_subtype hSemp

  let P : Ordinal → Ordinal → Prop := fun p q ↦ ∀ C ∈ S, (C ∩ Ioo p q).Nonempty
  have := @exists_seq_succ_prop o oLim P
  have aux : ∀ p < o, ∃ q < o, p < q ∧ P p q := fun p plto ↦ by
    have := exists_above_of_lt_cof plto nonemptyS (fun U hU ↦ (hS U hU).2) Scard
    exact this

  rcases exists_seq_succ_prop oLim aux qlto with ⟨f, hf⟩
  let g := fun p pltω ↦ (f p pltω).1

  have gInc : ∀ o h, g o h < g (o + 1) (omega_isLimit.succ_lt h) := fun o h ↦ hf.2.1 o h
  have bsuplt : bsup ω g < o := (bsup_lt_ord hCof) (fun i hi ↦ (f i hi).2)

  use bsup ω g
  constructor
  · apply mem_sInter.mpr
    intro C CmemS
    have := isAcc_bsup_of_between C omega_isLimit g gInc (fun i hi ↦ (hf.1 i hi) C CmemS)
    exact (hS C CmemS).1.2 ((bsup ω g)) bsuplt this
  · apply (lt_bsup g).mpr
    exact ⟨0, omega_pos, hf.2.2⟩

[Kim Morrison]

Just noting this is a PR now at #14060, and I've requested reviews from @Yaël Dillies and @Junyan Xu . :-)

[Yaël Dillies]

Something to read on the plane tomorrow!

[Nir Paz]

@Violeta Hernández Sorry I've been unavailable, I am free now and want to finish this pr. I know you want to change everything to Set (Iio o) instead of Set Ordinal, but I'm still not sure about this. Isn't adding this extra layer always going to make things a bit harder to work with?

For example if C is a subset of some o, stating that C ∩ p is a club in p:

-- C : Set Ordinal
IsClub (C ∩ (Iio p)) p

vs

-- C : Set (Iio o)
IsClub (fun x ↦ x.1 ∈ C : Set (Iio p)) -- am I missing an easier way?

Working on changing them, Set (Iio o) feels more rigid and harder to rw since there are a lot more Iio o inequalities than actual Ordinal inequalities.

Note that the Set Ordinal vs Set (Iio o) debate is diffirent from the Π p < o → vs Iio o → one, and I think we conflated them on the pr discussions.

Also thanks a lot for all the help with this pr!

[Nir Paz]

Actually even saying that S ⊆ T when they are sets of different Iio _'s seems messy.

[Violeta Hernández]

Hm. If you want to talk about different intersections of the same set being clubs with different ordinals, then I can see how the Set (Iio o) design doesn't work.

[Violeta Hernández]

The reason for advocating for that was so that you could use the topology on Iio o, but admittedly talking about Set s for s : Set α is often an antipattern. So if Set Ordinal works better, so be it.

[Violeta Hernández]

Here's an idea though, why restrict the sets to be a subset of some Iio o? You could have IsClub s o simply mean that s ∩ Iio o is closed and unbounded in o. Then, stating that s ∩ p is a club in another ordinal p is just IsClub s p.

[Violeta Hernández]

The nice thing about doing this is that Ordinal.IsClosed s o iff s ∩ Iio o is closed as a set in Iio o. Not sure if there's a nice way to write down that last part, but it would allow for correspondence with the topological definition without having to work with Set (Iio o) all the time.

[Violeta Hernández]

This should, hopefully, give you a pretty simple proof of isClosed_sInter, where you go to the topological world, use their version of isClosed_sInter, and cast back.

[Nir Paz]

I like that! I'll use this definition

[Nir Paz]

Working like this IsAcc and IsUnbounded almost coincide, so I'm removing IsUnbounded entirely

[Violeta Hernández]

A benefit of doing this I just thought of: we can now state results like "the range of a normal function f is a club set for f o for any limit o"

[Nir Paz]

So what's the right way to take the supremum of some f : Iio o → Ordinal.{u} where o : Ordinal.{u}? iSup is a universe too high (and I don't see a theorem giving something useful when the image is bounded) and Ordinal.sup requires the domain to be in a lower universe.
Is there something like sup : (ι → Ordinal.{u}) → Ordinal.{u} with theorems that assume Small.{u} ι?

[Violeta Hernández]

Ordinal.sup is on its way out for this exact reason, see #15820

[Violeta Hernández]

For the moment I think it's fine if you use bsup. That's getting ditched later down the line, but by then we'll have the necessary lemmas assuming Small.{u} ι.

[Nir Paz]

bsup is for f : Π a < o, Ordinal. do you mean taking the bsup of the corresponding Π-style function?

[Violeta Hernández]

Yeah.

[Violeta Hernández]

If you find bsup too inconvenient (which is kind of funny considering this is the one thing it was meant for), you can also simply use iSup together with docs#Ordinal.bddAbove_of_small and its related lemmas

[Yaël Dillies]

Well actually you will need an API for ⨆ i, ⨆ _ : p i, f i for functions ι → Ordinal.{u} such that Small.{u} {i : ι // p i}, Violeta. ι might not be u-small

[Violeta Hernández]

How often are we going to have a Small {i // p i} instance lying around, but not a Small i one?

[Yaël Dillies]

Anytime you take the supremum of a function f : Ordinal.{u} → Ordinal.{u} :grinning:

[Violeta Hernández]

Hmm... I was going to say Iio o for ordinal o was the only instance of this, but we might in theory want to index a supremum by some other kind of interval like Iic, or we might even want to index a supremum by cardinals or stuff like that.

[Violeta Hernández]

Yeah, I'll add that API alongside the universe-generalized iSup API.

[Nir Paz]

I proved this:

theorem isClosed_iff_isClosed {o : Ordinal} (olim : IsLimit o) (A : Set Ordinal)
    [TopologicalSpace (Iio o)] [OrderTopology (Iio o)] :
    Ordinal.IsClosed A o ↔ IsClosed (fun x ↦ x.1 ∈ A : Set (Iio o)) :=

Is this the right way to use the order topology? This is my first time touching this part of the library. Also if anyone sees a way to state this more easily I'd love that.

[Yaël Dillies]

Surely you don't need to assume [TopologicalSpace (Iio o)] [OrderTopology (Iio o)] since Iio o is a concrete type with those instances already existing?

[Nir Paz]

I thought it's weird but figuered since this determines the topology it might be how this is done. Then how do I "set" the order topology to be the one I use? I couldn't find any theorems about specific order topologies

[Kevin Buzzard]

I think Yael is suggesting that you just delete those assumptions because typeclass inference might already know them.

[Yaël Dillies]

The first instance is docs#instTopologicalSpaceSubtype. The second one seems to not exist?

[Nir Paz]

Kevin Buzzard said:

I think Yael is suggesting that you just delete those assumptions because typeclass inference might already know them.

hmm. So when before checking the proof, lean sees I use a theorem assuming an OrderTopology instance, and guesses that's the topology I'm talking about throughout the proof?

[Nir Paz]

Yaël Dillies said:

The first instance is docs#instTopologicalSpaceSubtype. The second one seems to not exist?

It does: orderTopology_of_ordConnected. Just removing the assumptions works

[Yaël Dillies]

Nir Paz said:

So when before checking the proof, lean sees I use a theorem assuming an OrderTopology instance, and guesses that's the topology I'm talking about throughout the proof?

Yes, the same way as you didn't have to assume [LinearOrder (Iio o)]. It is already an ambient fact

[Violeta Hernández]

Nir Paz said:

I proved this:

theorem isClosed_iff_isClosed {o : Ordinal} (olim : IsLimit o) (A : Set Ordinal)
    [TopologicalSpace (Iio o)] [OrderTopology (Iio o)] :
    Ordinal.IsClosed A o ↔ IsClosed (fun x ↦ x.1 ∈ A : Set (Iio o)) :=

Is this the right way to use the order topology? This is my first time touching this part of the library. Also if anyone sees a way to state this more easily I'd love that.

You shouldn't be writing sets using function notation. Use {x : Iio o | x.1 ∈ A) instead.

[Violeta Hernández]

But that's great! I think it'll be really convenient to switch back and forth between these notions.

[Connor Gordon]

A couple years ago for a class project I did some work in Lean 3 with club and stationary sets (proving an intersection of 2 clubs is club, and taking as a black box that an intersection of <kappa-many clubs on kappa is club, proving Fodor's lemma). The proofs are quite inefficient and definitely not up to style guidelines (I never ended up refactoring it for a mathlib PR), and also not in Lean 4, but perhaps some of the ideas here could help you avoid reinventing the wheel.

project1.lean
project2.lean

[Nir Paz]

That's really cool! I actually proved Fodor's a while back too, but the proof is so messy I'll probably have to redo it for mathlib.

[Violeta Hernández]

I'd love to see this kind of stuff in Mathlib, be sure to tag me if you ever make a PR and I'll gladly review :smile:

[Violeta Hernández]

Something I've wanted to do for quite a while now is to define the Veblen hierarchy. I already made docs#Ordinal.nfpFamily which gets us most of the way there, but this happens to touch on multiple aspects of the library that really need to be refactored, so I've been stuck

[Nir Paz]

With this it seems simple to define the enumeration of the common fixed points of a small set of normals. Is there a problematic part or have you just been waiting to save work when refactoring?

[Nir Paz]

Actually looking at more of the code, isn't Veblen just iterating derivFamily?

[Violeta Hernández]

Nir Paz said:

With this it seems simple to define the enumeration of the common fixed points of a small set of normals. Is there a problematic part or have you just been waiting to save work when refactoring?

The latter. I even have a mathlib3 branch out there where I set up the definitions, I think veblen. But I'm currently trying to refactor Ordinal.sup, and Ordinal.IsLimit, and later I'll be refactoring out the notions of "bounded families", and all of this impacts that.

[Violeta Hernández]

Also, the most direct definition of Veblen would actually use derivBFamily, but really what needs to be done instead is change the definition of derivFamily to take in a small type rather than a type in a smaller universe.

[Floris van Doorn]

@Theofanis Chatzidiamantis-Christoforidis, a past student of mine, also proved Fodor's lemma as a course project: https://github.com/thchatzidiamantis/LeanCourse23/blob/master/LeanCourse/Project/Fodor.lean#L763

[Violeta Hernández]

Heh, there's clearly interest in that result

[Theofanis Chatzidiamantis-Christoforidis]

Mine is probably the messiest of the proofs discussed above, but it includes all the painful induction.

[Nir Paz]

@Violeta Hernández Since the actual clubs file is so full of inconsistent uses of sup, isup and bsup I'm thinking of waiting for the refactor to push it to prevent unnecessary work.

[Nir Paz]

Actually I don't need the whole refactor obviously, just the sSup and iSup Small lemmas about Ordinals. Let me know when there's a branch with these!

[Violeta Hernández]

The refactor will take a bit. The initial PR #15820 has already been open for a month, and I'm expecting the bsup refactor to take even longer just because of how pervasive its uses are. I'm also concurrently working on other refactors, most notably with IsSuccLimit.

[Violeta Hernández]

I've actually wanted to do this sup thing since 2022, but I ended up leaving Lean until a few months ago because of burnout.