Documentation

PiBaseLean.Theorems.T201.Theorem

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

Theorem T201: P26 (SeparableSpace) + P55 (IsCompletelyMetrizableSpace) => P116 (PolishSpace)

source
theorem PiBase.Formal.T201 :
P26 ⊓ P55 ≤ P116