theorem PiBase.instLocallyCompactSpaceOfNoetherianSpace {X : Type u} [TopologicalSpace X] [TopologicalSpace.NoetherianSpace X] : LocallyCompactSpace X

Theorem T652: P208 (NoetherianSpace) => P130 (LocallyCompactSpace)

theorem PiBase.Formal.T652 : P208 ≤ P130