Transporting the k-Menger game along a homeomorphism

The k-Menger game is the gFinGame 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.kMengerGame_isPayoff_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (b : ℕ → Set (Set Y)) : (kMengerGame Y).IsPayoff b ↔ (kMengerGame X).IsPayoff fun (n : ℕ) => (preimageFamilyEquiv φ) (b n)

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

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

theorem PiBase.WellDefined.strategicallyKMengerSpace : WellDefined StrategicallyKMengerSpace