theorem PiBase.rothbergerGame_isPayoff_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (b : ℕ → Set (Set Y)) : (rothbergerGame Y).IsPayoff b ↔ (rothbergerGame X).IsPayoff fun (n : ℕ) => (preimageFamilyEquiv φ) (b n)

theorem PiBase.HasWinningStrategyB.rothbergerGame_of_homeomorph {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (h : HasWinningStrategyB (rothbergerGame X)) : HasWinningStrategyB (rothbergerGame Y)

theorem PiBase.HasMarkovKWinningStrategyB.rothbergerGame_of_homeomorph {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {k : ℕ} (φ : X ≃ₜ Y) (h : HasMarkovKWinningStrategyB (rothbergerGame X) k) : HasMarkovKWinningStrategyB (rothbergerGame Y) k

theorem PiBase.WellDefined.strategicallyRothbergerSpace : WellDefined StrategicallyRothbergerSpace