Documentation

PiBaseLean.Theorems.T147.Theorem

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

Theorem T147: P177 (SigmaSpace) => P117 (HasSigmaLocallyFiniteNetwork)

source
theorem PiBase.Formal.T147 :
P177 ≤ P117