Documentation

PiBaseLean.Properties.P78.Lemmas

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