Documentation

PiBaseLean.Theorems.T264.Theorem

source
theorem PiBase.instPseudoMetrizableSpaceOfMetrizableSpace {X : Type u} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] :
TopologicalSpace.PseudoMetrizableSpace X

Theorem T264: P53 (MetrizableSpace) => P121 (PseudoMetrizableSpace)

source
theorem PiBase.Formal.T264 :
P53 ≤ P121