Documentation

PiBaseLean.Theorems.T105.Theorem

source
theorem PiBase.instFullyT4SpaceOfT1SpaceOfFullyNormalSpace {X : Type u} [TopologicalSpace X] [T1Space X] [FullyNormalSpace X] :
FullyT4Space X

Theorem T105: P2 (T1Space) + P34 (FullyNormalSpace) => P35 (FullyT4Space)

source
theorem PiBase.Formal.T105 :
P2 ⊓ P34 ≤ P35