Documentation

PiBaseLean.Theorems.T150.Theorem

source
theorem PiBase.instSigmaSpaceOfHasSigmaLocallyFiniteNetworkOfT3Space {X : Type u} [TopologicalSpace X] [HasSigmaLocallyFiniteNetwork X] [T3Space X] :
SigmaSpace X

Theorem T150: P117 (HasSigmaLocallyFiniteNetwork) + P5 (T3Space) => P177 (SigmaSpace)

source
theorem PiBase.Formal.T150 :
P117 ⊓ P5 ≤ P177