Smallness from a cardinal bound

Stream: Is there code for X?

[Aaron Anderson]

Do we have any direct link between small and cardinal inequalities?

I think I may want (for Loewenheim-Skolem related hijinks) the fact that if the cardinality of a type is less than cardinal.univ.{w}, then my type is small. I bet I could prove this, but is it out there?

[Floris van Doorn]

I don't think we have it. docs#ordinal.bdd_above_iff_small is somewhat similar though.

[Aaron Anderson]

Ok then - hopefully this is the best way to express it #12887