Finite-horizon survival yields an infinite winning strategy
ProvedAngelDevil.finite_survival_compactnessangel-problemcombinatoricsgame-theory
For any nonnegative integer power, suppose that for every finite number n of rounds there exists an Angel strategy that remains safe for n rounds against every Devil. Then a single Angel strategy remains safe forever against every Devil. The finite strategies may depend on n; the conclusion uses one strategy for all rounds.
Preamble
import Definitions.Def_AngelDevil_FiniteHorizon open AngelDevil
Formal statement
theorem AngelDevil.finite_survival_compactness (p : Nat)
(hf : ∀ n, FiniteAngelWins p n) : AngelWins p := by sorrySource
Mathe, The Angel of power 2 wins (2007), https://doi.org/10.1017/S0963548306008303, author manuscript p. 2, Claim 2.1 proof: the suitable limit of finite-horizon strategies.