Documentation

PiBaseLean.Theorems.T818.Theorem

source
instance PiBase.instTorontoSpaceOfFinite {X : Type u_1} [TopologicalSpace X] [Finite X] :
TorontoSpace X
source
theorem PiBase.Formal.T818 :
P78 ≤ P219