Documentation

PiBaseLean.Theorems.T650.Theorem

source
theorem PiBase.instCompactSpaceOfNoetherianSpace {X : Type u} [TopologicalSpace X] [TopologicalSpace.NoetherianSpace X] :
CompactSpace X

Theorem T650: P208 (NoetherianSpace) => P16 (CompactSpace)

source
theorem PiBase.Formal.T650 :
P208 ≤ P16