IsStrongLimit

Stream: mathlib4

[Violeta Hernández]

We currently have the theorems docs#Cardinal.mk_bounded_subset and docs#Cardinal.mk_subset_mk_lt_cof which take in a ∀ x < #α, 2 ^ x < #α assumption. In other words, they require that either #α be a docs#Cardinal.IsStrongLimit or zero.

[Violeta Hernández]

Is this indication that IsStrongLimit should be redefined so that IsStrongLimit 0? Does this mean that we need a IsStrongPrelimit / IsStrongLimit split like we did with docs#IsSuccPrelimit / docs#IsSuccLimit ? Or are we ok just passing arguments like that to theorems?

[Violeta Hernández]

(Note that there's not a lot to go off since there currently aren't very many theorems on IsStrongLimit)

[Violeta Hernández]

@Nir Paz

[Nir Paz]

I don't think the strong limit definition should change, just because I assume using the alternative would yield approximately the same number of inconveniences as this definition.

I guess I don't mind a prelimit definition either way, but I'm totally fine passing this kind of assumption around without an explicit definition for it.

[Violeta Hernández]

I feel like that argument would apply to forall x < y, succ x < y as well, though...