Documentation

PiBaseLean.Theorems.T802.Theorem

source
theorem PiBase.instStoneSpaceOfStoneanSpace {X : Type u} [TopologicalSpace X] [StoneanSpace X] :
StoneSpace X

Theorem T802: P119 (StoneanSpace) => P195 (StoneSpace)

source
theorem PiBase.Formal.T802 :
P119 ≤ P195