inaccessible

Stream: general

[Violeta Hernández]

Yaël recently made me aware of inaccessible, an abandoned branch by @Floris van Doorn from 2019. I'm interested in reviving it and PR-ing it.

[Violeta Hernández]

What was the goal of this branch? Was it just to add a few theorems on cofinality?

[Violeta Hernández]

(Also, some help on the remaining theorems would be nice...)

[Floris van Doorn]

Yes, I just wanted to add some results about inaccessible cardinals. I don't think I had a specific goal in mind.

[Floris van Doorn]

branch#inaccessible

[Floris van Doorn]

For the two sorry's that I had remaining when I ended, cof_bsup_le_cof_of_nondecreasing has mathematically a very similar statement to cof_sup_le_cof and cof_bsup_eq is similar to cof_sup_eq_cof. I remember that I still had some difficulties in proving them, but maybe following a similar proof strategy helps.

[Floris van Doorn]

I hope this helps. Thanks for and good luck on reviving it!

[Violeta Hernández]

A few of these theorems had the assumption ∀ i, f i < sup f. As it turns out, these were actually theorems about least strict upper bounds, and I've restated them accordingly.

[Violeta Hernández]

With that said, I'm a bit skeptical about one of the yet-unproven statements:

theorem cof_lsub_eq_cof {ι} {r : ι → ι → Prop} [is_well_order ι r] (f : ι → ordinal)
  (hf : ∀ i j, r i j → f i ≤ f j) : cof (lsub.{u v} f) = (type r).lift.cof :=

[Violeta Hernández]

Well orders are supposed to be strict, right? If so, wouldn't the correct assumption be ∀ i j, r i j → f i < f j?

[Violeta Hernández]

Otherwise you'd get issues with constant functions.