Documentation

PiBaseLean.Properties.P57.Lemmas

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