Documentation

PiBaseLean.Theorems.T200.Theorem

source
theorem PiBase.instIsCompletelyMetrizableSpaceOfPolishSpace {X : Type u} [TopologicalSpace X] [PolishSpace X] :
TopologicalSpace.IsCompletelyMetrizableSpace X

Theorem T200: P116 (PolishSpace) => P55 (IsCompletelyMetrizableSpace)

source
theorem PiBase.Formal.T200 :
P116 ≤ P55