I was going through the proof of existence of a Nash Equilibria in finite normal form games (Proof via Brouwer’s theorem) and got a question regarding the requirement of finiteness for the number of actions a player can play. In particular, the proof hints at the update equations where players "compute" their payoffs/utility of playing a best response, before going deeper into Brouwer's. I would think that, in this framework, the number of actions needs to be finite otherwise it would be impossible to compute those "utility-updates"... but is it the main point? Or am I missing something?
Edit: The proof I am looking at is: https://www.cs.ubc.ca/cgi-bin/tr/2007/TR-2007-25.pdf. The update rules are in "Theorem 23".