class PiBase.MarkovRothbergerSpace (X : Type u) [TopologicalSpace X] : Prop

• markov_rothberger : Nonempty X → HasMarkovKWinningStrategyB (rothbergerGame X) 1