Documentation

PiBaseLean.Properties.P164.Lemmas

source
theorem PiBase.WellDefined.cardLtEveryMeasurableCardinal :
WellDefined fun (X : Type u) [TopologicalSpace X] => CardLtEveryMeasurableCardinal X