theorem PiBase.Formal.ofFun_map {M : Type u} {N : Type v} (g : M → N) (f : ℕ → M) (k : ℕ) : List.map g (List.ofFun f k) = List.ofFun (fun (n : ℕ) => g (f n)) k

Mapping an initial segment of a sequence is the initial segment of the mapped sequence.

theorem PiBase.Formal.ofAllowed_isPayoff_iff {M : Type u} {N : Type v} (Ψ : N → M) {G : Game M} {H : Game N} {S : AllowedMoves M} {T : AllowedMoves N} (hST : ∀ (l : List N), T l ↔ S (List.map Ψ l)) (hGH : ∀ (c : ℕ → N), H.IsPayoff c ↔ G.IsPayoff fun (n : ℕ) => Ψ (c n)) (b : ℕ → N) : (H.ofAllowed T).IsPayoff b ↔ (G.ofAllowed S).IsPayoff fun (n : ℕ) => Ψ (b n)

Transport of Game.ofAllowed payoffs along a map Ψ of the move type.

theorem PiBase.Formal.hasWinningStrategyA_of_comap {M : Type u} {N : Type v} (Ψ : N → M) (Φ : M → N) (hΨΦ : ∀ (p : M), Ψ (Φ p) = p) {G : Game M} {H : Game N} (hpay : ∀ (b : ℕ → N), H.IsPayoff b ↔ G.IsPayoff fun (n : ℕ) => Ψ (b n)) (h : HasWinningStrategyA G) : HasWinningStrategyA H

Transport a winning strategy for player A along a retraction Ψ ∘ Φ = id of the move type.

def PiBase.Formal.wMoveComap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (q : Y × Set Y) : X × Set X

The move of the wGame on X corresponding to a move of the wGame on Y along a homeomorphism φ : X ≃ₜ Y.

Equations

• PiBase.Formal.wMoveComap φ q = (φ.symm q.1, ⇑φ ⁻¹' q.2)

def PiBase.Formal.wMoveMap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (p : X × Set X) : Y × Set Y

The move of the wGame on Y corresponding to a move of the wGame on X along a homeomorphism φ : X ≃ₜ Y.

Equations

• PiBase.Formal.wMoveMap φ p = (φ p.1, ⇑φ '' p.2)

theorem PiBase.Formal.wMoveComap_wMoveMap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (p : X × Set X) : wMoveComap φ (wMoveMap φ p) = p

theorem PiBase.Formal.wMoveComap_default {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (y : Y) : wMoveComap φ (y, ∅) = (φ.symm y, ∅)

theorem PiBase.Formal.preimage_mem_nhds_symm_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (y : Y) (S : Set Y) : ⇑φ ⁻¹' S ∈ nhds (φ.symm y) ↔ S ∈ nhds y

theorem PiBase.Formal.wAllowed_comap_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (y : Y) (l : List (Y × Set Y)) : l ≠ [] → (Odd l.length → (l.getLastD (y, ∅)).2 ∈ nhds y) ∧ (Even l.length → (l.getLastD (y, ∅)).1 ∈ (l.dropLast.getLastD (y, ∅)).2) ↔ List.map (wMoveComap φ) l ≠ [] → (Odd (List.map (wMoveComap φ) l).length → ((List.map (wMoveComap φ) l).getLastD (φ.symm y, ∅)).2 ∈ nhds (φ.symm y)) ∧ (Even (List.map (wMoveComap φ) l).length → ((List.map (wMoveComap φ) l).getLastD (φ.symm y, ∅)).1 ∈ ((List.map (wMoveComap φ) l).dropLast.getLastD (φ.symm y, ∅)).2)

The allowed moves of the wGame at y correspond to the allowed moves of the wGame at φ.symm y under wMoveComap φ.

theorem PiBase.WellDefined.wSpace : WellDefined WSpace