Documentation

PiBaseLean.Theorems.T136.Theorem

source
theorem PiBase.instBaireSpaceOfWeaklyLocallyCompactSpaceOfRegularSpace {X : Type u} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [RegularSpace X] :
BaireSpace X

Theorem T136: P23 (WeaklyLocallyCompactSpace) + P11 (RegularSpace) => P64 (BaireSpace)

source
theorem PiBase.Formal.T136 :
P23 ⊓ P11 ≤ P64