class PiBase.ProximalSpace (X : Type u) [τ : TopologicalSpace X] : Prop

• proximal (h : Inhabited X) : ∃ (t : UniformSpace X), t.toTopologicalSpace = τ ∧ HasWinningStrategyA (proximalGame X)