instance PiBase.instPartitionTopologyOfIndiscreteTopology {X : Type u} [TopologicalSpace X] [h : IndiscreteTopology X] : PartitionTopology X

Theorem T448: P129 (IndiscreteTopology) => P185 (PartitionTopology)

theorem PiBase.Formal.T448 : P129 ≤ P185