Transporting the k-Rothberger game along a homeomorphism

The k-Rothberger game is the g1Game played with k-covers, so the transport machinery of PiBaseLean.Properties.P151.Defs applies verbatim once we know that being a k-cover is invariant under a homeomorphism (preimageFamilyEquiv_isKCover').

theorem PiBase.preimageFamilyEquiv_mem_kCovers {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (S : Set (Set Y)) : (preimageFamilyEquiv φ) S ∈ {A : Set (Set X) | IsKCover' A} ↔ S ∈ {A : Set (Set Y) | IsKCover' A}

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

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

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

theorem PiBase.WellDefined.strategicallyKRothbergerSpace : WellDefined StrategicallyKRothbergerSpace