class PiBase.Lots (X : Type u_1) [TopologicalSpace X] : Prop

• from_linear_order : ∃ (x : LinearOrder X), OrderTopology X