This file builds up defs and basic theory about Gale-Stewart games. This has been done previously in Lean, for example here https://afm.episciences.org/17712/pdf

Additionally, we define various topological games.

For a reference on the theory, see https://en.wikipedia.org/wiki/Determinacy

For topological games, see https://en.wikipedia.org/wiki/Topological_game

def List.ofFun {α : Type u} (f : ℕ → α) : ℕ → List α

Given some function f : ℕ → X and some natural number n, the list of the form (f(0), f(1), ..., f(n - 1)).

Equations

• List.ofFun f 0 = []
• List.ofFun f n.succ = List.ofFun f n ++ [f n]

@[simp]

theorem List.ofFun_length {α : Type u} (f : ℕ → α) (n : ℕ) : (ofFun f n).length = n

def List.ltakeHalf {α : Type u} : List α → ℕ → List α

Equations

• x✝.ltakeHalf 0 = []
• [].ltakeHalf n.succ = []
• [a].ltakeHalf n.succ = [a]
• (a :: head :: l).ltakeHalf n.succ = a :: l.ltakeHalf n

def List.rtakeHalf {α : Type u} (l : List α) (n : ℕ) : List α

The n most recent moves by the opponent in a chronological game history, listed from newest to oldest.

Equations

• l.rtakeHalf n = l.reverse.ltakeHalf n

structure PiBase.Game (X : Type u) : Type u

A game on some type X. Abstractly, this is equivalent to Set (ℕ → X).

• IsPayoff (a : ℕ → X) : Prop

  Whether player A wins on some game.

def PiBase.WinningStrategyA {X : Type u} (G : Game X) (f : List X → X) : Prop

On a low level, a strategy is just a function f : List X → X. We say a function is a winning strategy for Player A, if Player A wins the game f([]), a₁, f([a₁]), a₂, ... is payoff.

Equations

• PiBase.WinningStrategyA G f = ∀ (b : ℕ → X), (∀ (n : ℕ), b (2 * n) = f (List.ofFun b (2 * n))) → G.IsPayoff b

def PiBase.MarkovKWinningStrategyA {X : Type u} (G : Game X) (f : ℕ → List X → X) (k : ℕ) : Prop

Equations

• PiBase.MarkovKWinningStrategyA G f k = ∀ (b : ℕ → X), (∀ (n : ℕ), b (2 * n) = f n ((List.ofFun b (2 * n)).rtakeHalf k)) → G.IsPayoff b

def PiBase.WinningStrategyB {X : Type u} (G : Game X) (f : List X → X) : Prop

A winning strategy for Player B. Note that it is possible neither A nor B have a winning strategy.

Equations

• PiBase.WinningStrategyB G f = ∀ (b : ℕ → X), (∀ (n : ℕ), b (2 * n + 1) = f (List.ofFun b (2 * n + 1))) → ¬G.IsPayoff b

def PiBase.MarkovKWinningStrategyB {X : Type u} (G : Game X) (f : ℕ → List X → X) (k : ℕ) : Prop

Equations

• PiBase.MarkovKWinningStrategyB G f k = ∀ (b : ℕ → X), (∀ (n : ℕ), b (2 * n + 1) = f n ((List.ofFun b (2 * n + 1)).rtakeHalf k)) → ¬G.IsPayoff b

def PiBase.HasWinningStrategyA {X : Type u} (G : Game X) : Prop

Equations

• PiBase.HasWinningStrategyA G = ∃ (f : List X → X), PiBase.WinningStrategyA G f

def PiBase.HasMarkovKWinningStrategyA {X : Type u} (G : Game X) (k : ℕ) : Prop

We say Player A has a k-Markov winning strategy, if they have a winning strategy only depending on the round number and the k most recent moves by the opponent.

Equations

• PiBase.HasMarkovKWinningStrategyA G k = ∃ (f : ℕ → List X → X), PiBase.MarkovKWinningStrategyA G f k

def PiBase.HasWinningStrategyB {X : Type u} (G : Game X) : Prop

Equations

• PiBase.HasWinningStrategyB G = ∃ (f : List X → X), PiBase.WinningStrategyB G f

def PiBase.HasMarkovKWinningStrategyB {X : Type u} (G : Game X) (k : ℕ) : Prop

We say Player B has a k-Markov winning strategy, if they have a winning strategy only depending on the round number and the k most recent moves by the opponent.

Equations

• PiBase.HasMarkovKWinningStrategyB G k = ∃ (f : ℕ → List X → X), PiBase.MarkovKWinningStrategyB G f k

def PiBase.MarkovKStrategy.toStrategy {X : Type u} (f : ℕ → List X → X) (k : ℕ) : List X → X

Equations

• PiBase.MarkovKStrategy.toStrategy f k l = f (l.length / 2) (l.rtakeHalf k)

theorem PiBase.MarkovKWinningStrategyA.winningStrategyA {X : Type u} (G : Game X) {f : ℕ → List X → X} {k : ℕ} (hf : MarkovKWinningStrategyA G f k) : WinningStrategyA G (MarkovKStrategy.toStrategy f k)

theorem PiBase.HasMarkovKWinningStrategyA.hasWinningStrategyA {X : Type u} (G : Game X) {k : ℕ} (h : HasMarkovKWinningStrategyA G k) : HasWinningStrategyA G

theorem PiBase.MarkovKWinningStrategyA.winningStrategyB {X : Type u} (G : Game X) {f : ℕ → List X → X} {k : ℕ} (hf : MarkovKWinningStrategyB G f k) : WinningStrategyB G (MarkovKStrategy.toStrategy f k)

theorem PiBase.HasMarkovKWinningStrategyB.hasWinningStrategyB {X : Type u} (G : Game X) {k : ℕ} (h : HasMarkovKWinningStrategyB G k) : HasWinningStrategyB G

@[reducible, inline]

abbrev PiBase.AllowedMoves (X : Type u) : Type u

Equations

• PiBase.AllowedMoves X = (List X → Prop)

def PiBase.Game.ofAllowed {X : Type u} (G : Game X) (S : AllowedMoves X) : Game X

Usually, a game has some "allowed" moves, which the players can do. If they make a disallowed move, they lose immediately. This auxiliary definition is meant to formalise this behaviour.

In particle we use this definition to describe the "winning argument" in G and the allowed moves in S.

Equations

• One or more equations did not get rendered due to their size.

def PiBase.banachMazur (X : Type u) (S : Set X) (W : Set (Set X)) : Game (Set X)

Banach Mazur game. Usually there are conditions on X (should be topological space) and W (each member ought to have nonempty interior), but this isn't needed for the definition.

Equations

• PiBase.banachMazur X S W = { IsPayoff := fun (s : ℕ → Set X) => (S ∩ ⋂ (i : ℕ), s i).Nonempty }.ofAllowed fun (l : List (Set X)) => (∀ i ∈ l, i ∈ W) ∧ ∀ i ∈ l, l.getLastD ∅ ⊆ i

def PiBase.g1Game {X : Type u} (A B : Set (Set X)) : Game (Set X)

Equations

• One or more equations did not get rendered due to their size.

def PiBase.gFinGame {X : Type u} (A B : Set (Set X)) : Game (Set X)

Equations

• One or more equations did not get rendered due to their size.

def PiBase.rothbergerGame (X : Type u) [TopologicalSpace X] : Game (Set (Set X))

See https://www.sciencedirect.com/science/article/pii/S016686411830470X

Equations

• PiBase.rothbergerGame X = PiBase.g1Game {A : Set (Set X) | ⋃₀ A = Set.univ ∧ ∀ s ∈ A, IsOpen s} {A : Set (Set X) | ⋃₀ A = Set.univ ∧ ∀ s ∈ A, IsOpen s}

def PiBase.mengerGame (X : Type u) [TopologicalSpace X] : Game (Set (Set X))

See https://www.sciencedirect.com/science/article/pii/S016686411830470X

Equations

• PiBase.mengerGame X = PiBase.gFinGame {A : Set (Set X) | ⋃₀ A = Set.univ ∧ ∀ s ∈ A, IsOpen s} {A : Set (Set X) | ⋃₀ A = Set.univ ∧ ∀ s ∈ A, IsOpen s}

def PiBase.kMengerGame (X : Type u) [TopologicalSpace X] : Game (Set (Set X))

See https://www.sciencedirect.com/science/article/pii/S0166864121001863

Equations

• PiBase.kMengerGame X = PiBase.gFinGame {A : Set (Set X) | PiBase.IsKCover' A} {A : Set (Set X) | PiBase.IsKCover' A}

def PiBase.kRothbergerGame (X : Type u) [TopologicalSpace X] : Game (Set (Set X))

See https://www.sciencedirect.com/science/article/pii/S0166864121001863

Equations

• PiBase.kRothbergerGame X = PiBase.g1Game {A : Set (Set X) | PiBase.IsKCover' A} {A : Set (Set X) | PiBase.IsKCover' A}

def PiBase.wGame {X : Type u} [TopologicalSpace X] (x : X) : Game (X × Set X)

See https://topology.pi-base.org/properties/P187

Equations

• One or more equations did not get rendered due to their size.

def PiBase.strongChoquetGame (X : Type u) [TopologicalSpace X] [Inhabited X] : Game (X × Set X)

See https://topology.pi-base.org/properties/P206

Equations

• One or more equations did not get rendered due to their size.

def PiBase.proximalGame (X : Type u) [UniformSpace X] [Inhabited X] : Game (X × Set (X × X))

The proximal game. The condition Inhabited X is an implementation detail; in theory it could also be played on the empty space, but that makes the lean definition much uglier.

Equations

• One or more equations did not get rendered due to their size.

theorem PiBase.map_ofFun {A : Type u} {B : Type v} (e : B → A) (b : ℕ → B) (k : ℕ) : List.map e (List.ofFun b k) = List.ofFun (fun (n : ℕ) => e (b n)) k

theorem PiBase.map_ltakeHalf {A : Type u} {B : Type v} (e : B → A) (l : List B) (n : ℕ) : List.map e (l.ltakeHalf n) = (List.map e l).ltakeHalf n

theorem PiBase.map_rtakeHalf {A : Type u} {B : Type v} (e : B → A) (l : List B) (n : ℕ) : List.map e (l.rtakeHalf n) = (List.map e l).rtakeHalf n

theorem PiBase.isPayoff_ofAllowed_iff {A : Type u} {B : Type v} {G : Game A} {H : Game B} {SA : AllowedMoves A} {SB : AllowedMoves B} (e : B → A) (hS : ∀ (l : List B), SB l ↔ SA (List.map e l)) (b : ℕ → B) (hP : H.IsPayoff b ↔ G.IsPayoff fun (n : ℕ) => e (b n)) : (H.ofAllowed SB).IsPayoff b ↔ (G.ofAllowed SA).IsPayoff fun (n : ℕ) => e (b n)

Transport of a payoff condition through a relabelling e of the moves, for games built with Game.ofAllowed.

theorem PiBase.HasWinningStrategyA.of_equiv {A : Type u} {B : Type v} {G : Game A} {H : Game B} (e : B ≃ A) (hP : ∀ (b : ℕ → B), (G.IsPayoff fun (n : ℕ) => e (b n)) → H.IsPayoff b) (hG : HasWinningStrategyA G) : HasWinningStrategyA H

Transport a winning strategy for player A along an equivalence of moves.

theorem PiBase.HasWinningStrategyB.of_equiv {A : Type u} {B : Type v} {G : Game A} {H : Game B} (e : B ≃ A) (hP : ∀ (b : ℕ → B), H.IsPayoff b → G.IsPayoff fun (n : ℕ) => e (b n)) (hG : HasWinningStrategyB G) : HasWinningStrategyB H

Transport a winning strategy for player B along an equivalence of moves.

theorem PiBase.HasMarkovKWinningStrategyB.of_equiv {A : Type u} {B : Type v} {G : Game A} {H : Game B} {k : ℕ} (e : B ≃ A) (hP : ∀ (b : ℕ → B), H.IsPayoff b → G.IsPayoff fun (n : ℕ) => e (b n)) (hG : HasMarkovKWinningStrategyB G k) : HasMarkovKWinningStrategyB H k

The k-Markov analogue of HasWinningStrategyB.of_equiv.

theorem PiBase.familyEquiv_apply {V : Type u} {W : Type v} (e : V ≃ W) (S : Set V) : (Equiv.Set.congr e) S = ⇑e '' S

theorem PiBase.familyEquiv_symm_apply {V : Type u} {W : Type v} (e : V ≃ W) (T : Set W) : (Equiv.Set.congr e).symm T = ⇑e.symm '' T

@[simp]

theorem PiBase.familyEquiv_empty {V : Type u} {W : Type v} (e : V ≃ W) : (Equiv.Set.congr e) ∅ = ∅

theorem PiBase.familyEquiv_mem_iff {V : Type u} {W : Type v} (e : V ≃ W) {S : Set V} {a : V} : e a ∈ (Equiv.Set.congr e) S ↔ a ∈ S

theorem PiBase.familyEquiv_singleton {V : Type u} {W : Type v} (e : V ≃ W) (a : V) : (Equiv.Set.congr e) {a} = {e a}

theorem PiBase.familyEquiv_iUnion {V : Type u} {W : Type v} (e : V ≃ W) (s : ℕ → Set V) : (Equiv.Set.congr e) (⋃ (n : ℕ), s n) = ⋃ (n : ℕ), (Equiv.Set.congr e) (s n)

@[simp]

theorem PiBase.familyEquiv_finite {V : Type u} {W : Type v} (e : V ≃ W) (S : Set V) : ((Equiv.Set.congr e) S).Finite ↔ S.Finite

@[simp]

theorem PiBase.familyEquiv_subset {V : Type u} {W : Type v} (e : V ≃ W) (S T : Set V) : (Equiv.Set.congr e) S ⊆ (Equiv.Set.congr e) T ↔ S ⊆ T

theorem PiBase.familyEquiv_exists_singleton {V : Type u} {W : Type v} (e : V ≃ W) (S T : Set V) : (∃ (a : W), (Equiv.Set.congr e) S = {a} ∧ a ∈ (Equiv.Set.congr e) T) ↔ ∃ (a : V), S = {a} ∧ a ∈ T

def PiBase.g1Allowed {V : Type u_1} (A : Set (Set V)) : AllowedMoves (Set V)

The allowed moves of a g1Game.

Equations

• PiBase.g1Allowed A l = (l ≠ [] → (Odd l.length → l.getLastD ∅ ∈ A) ∧ (Even l.length → ∃ (a : V), l.getLastD ∅ = {a} ∧ a ∈ l.dropLast.getLastD ∅))

def PiBase.gFinAllowed {V : Type u_1} (A : Set (Set V)) : AllowedMoves (Set V)

The allowed moves of a gFinGame.

Equations

• PiBase.gFinAllowed A l = (l ≠ [] → (Odd l.length → l.getLastD ∅ ∈ A) ∧ (Even l.length → (l.getLastD ∅).Finite ∧ l.getLastD ∅ ⊆ l.dropLast.getLastD ∅))

theorem PiBase.g1Allowed_iff {V : Type u} {W : Type v} (e : V ≃ W) {A : Set (Set V)} {A' : Set (Set W)} (hA : ∀ (S : Set V), (Equiv.Set.congr e) S ∈ A' ↔ S ∈ A) (l : List (Set V)) : g1Allowed A l ↔ g1Allowed A' (List.map (⇑(Equiv.Set.congr e)) l)

theorem PiBase.gFinAllowed_iff {V : Type u} {W : Type v} (e : V ≃ W) {A : Set (Set V)} {A' : Set (Set W)} (hA : ∀ (S : Set V), (Equiv.Set.congr e) S ∈ A' ↔ S ∈ A) (l : List (Set V)) : gFinAllowed A l ↔ gFinAllowed A' (List.map (⇑(Equiv.Set.congr e)) l)

theorem PiBase.selectionPayoff_iff {V : Type u} {W : Type v} (e : V ≃ W) {B : Set (Set V)} {B' : Set (Set W)} (hB : ∀ (S : Set V), (Equiv.Set.congr e) S ∈ B' ↔ S ∈ B) (b : ℕ → Set V) : ⋃ (n : ℕ), b (2 * n + 1) ∉ B ↔ ⋃ (n : ℕ), (Equiv.Set.congr e) (b (2 * n + 1)) ∉ B'

theorem PiBase.g1Game_isPayoff_iff {V : Type u} {W : Type v} (e : V ≃ W) {A : Set (Set V)} {A' : Set (Set W)} {B : Set (Set V)} {B' : Set (Set W)} (hA : ∀ (S : Set V), (Equiv.Set.congr e) S ∈ A' ↔ S ∈ A) (hB : ∀ (S : Set V), (Equiv.Set.congr e) S ∈ B' ↔ S ∈ B) (b : ℕ → Set V) : (g1Game A B).IsPayoff b ↔ (g1Game A' B').IsPayoff fun (n : ℕ) => (Equiv.Set.congr e) (b n)

theorem PiBase.gFinGame_isPayoff_iff {V : Type u} {W : Type v} (e : V ≃ W) {A : Set (Set V)} {A' : Set (Set W)} {B : Set (Set V)} {B' : Set (Set W)} (hA : ∀ (S : Set V), (Equiv.Set.congr e) S ∈ A' ↔ S ∈ A) (hB : ∀ (S : Set V), (Equiv.Set.congr e) S ∈ B' ↔ S ∈ B) (b : ℕ → Set V) : (gFinGame A B).IsPayoff b ↔ (gFinGame A' B').IsPayoff fun (n : ℕ) => (Equiv.Set.congr e) (b n)

Transporting topological move families

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

Taking preimages under a homeomorphism is a bijection between subsets.

Equations

• PiBase.preimageSetEquiv φ = { toFun := fun (t : Set Y) => ⇑φ ⁻¹' t, invFun := fun (s : Set X) => ⇑φ.symm ⁻¹' s, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem PiBase.preimageSetEquiv_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (t : Set Y) : (preimageSetEquiv φ) t = ⇑φ ⁻¹' t

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

Taking preimages under a homeomorphism is a bijection between families of subsets.

Equations

• PiBase.preimageFamilyEquiv φ = Equiv.Set.congr (PiBase.preimageSetEquiv φ)

theorem PiBase.preimageFamilyEquiv_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (S : Set (Set Y)) : (preimageFamilyEquiv φ) S = ⇑(preimageSetEquiv φ) '' S

@[simp]

theorem PiBase.preimageFamilyEquiv_empty {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) : (preimageFamilyEquiv φ) ∅ = ∅

theorem PiBase.sUnion_preimageFamilyEquiv {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (S : Set (Set Y)) : ⋃₀ (preimageFamilyEquiv φ) S = ⇑φ ⁻¹' ⋃₀ S

theorem PiBase.preimageFamilyEquiv_iUnion {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (s : ℕ → Set (Set Y)) : (preimageFamilyEquiv φ) (⋃ (n : ℕ), s n) = ⋃ (n : ℕ), (preimageFamilyEquiv φ) (s n)

@[simp]

theorem PiBase.preimageFamilyEquiv_finite {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (S : Set (Set Y)) : ((preimageFamilyEquiv φ) S).Finite ↔ S.Finite

@[simp]

theorem PiBase.preimageFamilyEquiv_subset {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (S T : Set (Set Y)) : (preimageFamilyEquiv φ) S ⊆ (preimageFamilyEquiv φ) T ↔ S ⊆ T

theorem PiBase.preimage_eq_univ_iff_of_homeomorph {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (U : Set Y) : ⇑φ ⁻¹' U = Set.univ ↔ U = Set.univ

@[simp]

theorem PiBase.preimageFamilyEquiv_mem_openCovers {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (S : Set (Set Y)) : (⋃₀ (preimageFamilyEquiv φ) S = Set.univ ∧ ∀ s ∈ (preimageFamilyEquiv φ) S, IsOpen s) ↔ ⋃₀ S = Set.univ ∧ ∀ t ∈ S, IsOpen t

theorem PiBase.preimageFamilyEquiv_eq {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) : preimageFamilyEquiv φ = Equiv.Set.congr (preimageSetEquiv φ)

theorem PiBase.preimageFamilyEquiv_mem_openCovers' {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (S : Set (Set Y)) : (preimageFamilyEquiv φ) S ∈ {A : Set (Set X) | ⋃₀ A = Set.univ ∧ ∀ s ∈ A, IsOpen s} ↔ S ∈ {A : Set (Set Y) | ⋃₀ A = Set.univ ∧ ∀ s ∈ A, IsOpen s}

theorem PiBase.preimageFamilyEquiv_univ_mem_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (S : Set (Set Y)) : Set.univ ∈ (preimageFamilyEquiv φ) S ↔ Set.univ ∈ S

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

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

The payoff conditions of the Menger games correspond under a homeomorphism.

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

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

@[simp]

theorem PiBase.prodMap_symm_prodMap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (p : X × X) : Prod.map (⇑φ.symm) (⇑φ.symm) (Prod.map (⇑φ) (⇑φ) p) = p

@[simp]

theorem PiBase.prodMap_prodMap_symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (p : Y × Y) : Prod.map (⇑φ) (⇑φ) (Prod.map (⇑φ.symm) (⇑φ.symm) p) = p

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

Equations

• PiBase.preimageRelEquiv φ = { toFun := fun (V : Set (Y × Y)) => Prod.map ⇑φ ⇑φ ⁻¹' V, invFun := fun (U : Set (X × X)) => Prod.map ⇑φ.symm ⇑φ.symm ⁻¹' U, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem PiBase.preimageRelEquiv_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (V : Set (Y × Y)) : (preimageRelEquiv φ) V = Prod.map ⇑φ ⇑φ ⁻¹' V

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

Equations

• PiBase.proximalMoveEquiv φ = φ.symm.prodCongr (PiBase.preimageRelEquiv φ)

@[simp]

theorem PiBase.proximalMoveEquiv_fst {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (p : Y × Set (Y × Y)) : ((proximalMoveEquiv φ) p).1 = φ.symm p.1

@[simp]

theorem PiBase.proximalMoveEquiv_snd {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (p : Y × Set (Y × Y)) : ((proximalMoveEquiv φ) p).2 = Prod.map ⇑φ ⇑φ ⁻¹' p.2

theorem PiBase.prodMap_surjective {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) : Function.Surjective (Prod.map ⇑φ ⇑φ)

@[simp]

theorem PiBase.preimage_prodMap_subset_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (V W : Set (Y × Y)) : Prod.map ⇑φ ⇑φ ⁻¹' V ⊆ Prod.map ⇑φ ⇑φ ⁻¹' W ↔ V ⊆ W

@[simp]

theorem PiBase.preimage_prodMap_eq_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (V W : Set (Y × Y)) : Prod.map ⇑φ ⇑φ ⁻¹' V = Prod.map ⇑φ ⇑φ ⁻¹' W ↔ V = W

theorem PiBase.preimage_eq_empty_iff_of_homeomorph {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (S : Set Y) : ⇑φ ⁻¹' S = ∅ ↔ S = ∅

theorem PiBase.slice_preimage_prodMap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (y : Y) (V : Set (Y × Y)) : Prod.mk (φ.symm y) ⁻¹' Prod.map ⇑φ ⇑φ ⁻¹' V = ⇑φ ⁻¹' Prod.mk y ⁻¹' V

theorem PiBase.exists_tendsto_comp_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (φ : X ≃ₜ Y) (f : ℕ → Y) : (∃ (z : X), Filter.Tendsto (fun (n : ℕ) => φ.symm (f n)) Filter.atTop (nhds z)) ↔ ∃ (z : Y), Filter.Tendsto f Filter.atTop (nhds z)