class PiBase.CardLtEveryMeasurableCardinal (X : Type u) : Prop

• card_lt_every_measurable (k : Cardinal.{u}) : IsMeasurable k → Cardinal.mk X < k