Documentation

PiBaseLean.Theorems.T251.Theorem

source
theorem PiBase.instCompactSpaceOfIndiscreteTopology {X : Type u} [TopologicalSpace X] [IndiscreteTopology X] :
CompactSpace X

Theorem T251: P129 (IndiscreteTopology) => P16 (CompactSpace)

source
theorem PiBase.Formal.T251 :
P129 ≤ P16