instance PiBase.instIndiscreteTopologyOfPartitionTopologyOfPreconnectedSpace {X : Type u} [TopologicalSpace X] [h : PartitionTopology X] [h' : PreconnectedSpace X] : IndiscreteTopology X

Theorem T468: P185 (PartitionTopology) + P36 (PreconnectedSpace) => P129 (IndiscreteTopology)

theorem PiBase.Formal.T468 : P185 ⊓ P36 ≤ P129