Documentation

PiBaseLean.Theorems.T86.Theorem

source
instance PiBase.instFunctionallyT2SpaceOfT25Space {X : Type u_1} [TopologicalSpace X] [h : FunctionallyT2Space X] :
T25Space X
source
theorem PiBase.Formal.T86 :
P9 ≤ P4